Events

Upcoming events

Functional Synthesis: An Ideal Meeting Ground for Formal Methods and Machine Learning

Kuldeep Meel National University of Singapore
29 Mar 2021, 10:00 am - 11:00 am
Virtual talk
SWS Colloquium
Don't we all dream of the perfect assistant whom we can just tell what to do and the assistant can figure out how to accomplish the tasks? Formally, given a specification F(X,Y) over the set of input variables X and output variables Y, we want the assistant, aka functional synthesis engine, to design a function G such that (X,Y=G(X)) satisfies F. Functional synthesis has been studied for over 150 years, dating back Boole in 1850's and yet scalability remains a core challenge. …
Don't we all dream of the perfect assistant whom we can just tell what to do and the assistant can figure out how to accomplish the tasks? Formally, given a specification F(X,Y) over the set of input variables X and output variables Y, we want the assistant, aka functional synthesis engine, to design a function G such that (X,Y=G(X)) satisfies F. Functional synthesis has been studied for over 150 years, dating back Boole in 1850's and yet scalability remains a core challenge. Motivated by progress in machine learning, we design a new algorithmic framework Manthan, which views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.

Please contact MPI-SWS office team for link information
Read more

Recent events

Human Factors in Secure Software Development: How we can help developers write secure code

Yasemin Acar MPI-SP
11 Mar 2021, 10:00 am - 11:00 am
Virtual talk
CIS@MPG Tenure-Track Faculty Recruiting
We are seeing a persistent gap between the theoretical security of e.g. cryptographic algorithms and real world vulnerabilities, data-breaches and possible attacks. Software developers – despite being computer experts – are rarely security experts, and security and privacy are usually, at best, of secondary importance for them. They may not have training in security and privacy or even be aware of the possible implications, and they may be unable to allocate time or effort to ensure that security and privacy best practices and design principles are upheld for their end users. …
We are seeing a persistent gap between the theoretical security of e.g. cryptographic algorithms and real world vulnerabilities, data-breaches and possible attacks. Software developers – despite being computer experts – are rarely security experts, and security and privacy are usually, at best, of secondary importance for them. They may not have training in security and privacy or even be aware of the possible implications, and they may be unable to allocate time or effort to ensure that security and privacy best practices and design principles are upheld for their end users. Understanding their education and mindsets, their processes, the tools that they use, and their pitfalls are the foundation for shifting development practices to be more secure. This talk will give an overview of security challenges for developers, and interdisciplinary research avenues to address these.

--

Please contact MPI-SWS Office team for link information.
Read more

Automatic Vulnerability Discovery at Scale

Marcel Böhme Monash University, Australia
09 Mar 2021, 10:00 am - 11:00 am
Virtual talk
CIS@MPG Tenure-Track Faculty Recruiting
To establish software security at scale, we need efficient automated vulnerability discovery techniques that can run on thousands of machines. In this talk, we will discuss the abundant opportunities and fundamental limitations of fuzzing, one of the most successful vulnerability discovery techniques. We will explore why only an exponential number of machines will allow us to discover software bugs at a linear rate. We will discuss the kind of correctness guarantees that we can expect from automatic vulnerability discovery, …
To establish software security at scale, we need efficient automated vulnerability discovery techniques that can run on thousands of machines. In this talk, we will discuss the abundant opportunities and fundamental limitations of fuzzing, one of the most successful vulnerability discovery techniques. We will explore why only an exponential number of machines will allow us to discover software bugs at a linear rate. We will discuss the kind of correctness guarantees that we can expect from automatic vulnerability discovery, anywhere from formally proving the absence of bugs to statistical claims about program correctness. We shall touch upon unexpected connections to ecological biostatistics and information theory which allow us to address long-standing scientific and practical problems in automatic software testing. Finally, we will take a forward looking view and discuss our larger vision for the field of software security.

--

Please contact MPI-SWS Office for Zoom link information
Read more

Exterminating bugs in real systems

Fraser Brown Stanford
08 Mar 2021, 3:00 pm - 4:00 pm
Virtual talk
CIS@MPG Tenure-Track Faculty Recruiting
Software is everywhere, and almost everywhere, software is broken. Some bugs just crash your printer; others hand an identity thief your bank account number; still others let nation-states spy on dissidents and persecute minorities. This talk outlines my work preventing bugs using a blend of programming languages techniques and systems design. First, I'll talk about securing massive, security-critical codebases without clean slate rewrites. This means rooting out hard-to-find bugs---as in Sys, which scales symbolic execution to find exploitable bugs in systems like the twenty-million line Chrome browser. …
Software is everywhere, and almost everywhere, software is broken. Some bugs just crash your printer; others hand an identity thief your bank account number; still others let nation-states spy on dissidents and persecute minorities. This talk outlines my work preventing bugs using a blend of programming languages techniques and systems design. First, I'll talk about securing massive, security-critical codebases without clean slate rewrites. This means rooting out hard-to-find bugs---as in Sys, which scales symbolic execution to find exploitable bugs in systems like the twenty-million line Chrome browser. It also means proving correctness of especially vulnerable pieces of code---as in VeRA, which automatically verifies part of the Firefox JavaScript engine. Finally, I'll discuss work on stronger foundations for new systems---as in CirC, a recent project unifying compiler infrastructure for program verification, cryptographic proofs, optimization problems, and more.

--

Please contact MPI-SWS Office for link information
Read more

Archive