This page contains a description of the invited talks and a list of accepted papers at CSF 2020.
Amal Ahmed - Secure Compilation: Challenges for the Next Decade
Secure compilation is aimed at building compilers and toolchains that preserve security properties of the source code they take as input in the target code they produce as output, thus ensuring soundness of source-level reasoning about security properties. To date, most work on secure compilation has focused on fully abstract compilation which guarantees that if two source components are observationally equivalent when run in any source context, then their compiled versions will be observationally equivalent when run in any target context (i.e., when interacting with any attacker code). Fully abstract compilers for realistic languages were once considered impossible since they require, in essence, that every target attacker's behavior is already expressible in the source language. But in the last decade we have seen new techniques for statically and dynamically enforcing and proving full abstraction by limiting how target contexts may interact with compiled code.
In the next decade, we should aim to develop end-to-end secure-compilation toolchains for all software where programmers need to reason about some security property. This requires tackling five significant challenges. Security DSLs: we need languages that allow programmers to express the security properties they care about so compilers know what properties to preserve and where to trade performance for security. Interoperability: code from safe/secure languages should compose with code from less safe languages without sacrificing security guarantees. Performance: enforcing security with acceptable overheads is critical and may require hardware support. Verification: we need proof methods for secure compilation that can be applied across the software toolchain; methods from fully abstract compilation may help. End-to-end security: we want to preserve security guarantees across the entire software-hardware stack, which will require formal models of security leaks via micro-architectural state and compilers that protect against such leaks. I'll discuss these challenges and how to structure future research efforts to build formally secure and performant compilers.
Dan Boneh - New opportunities for formal verification in cryptography
In recent years there has been tremendous progress in the development of protocols for succinct non-interactive arguments of knowledge, called SNARKs. This progress generated considerable real-world interest, and there are now implemented SNARKs capable of handling statements involving many millions of arithmetic gates (e.g., libsnark, Bellman, Circom, Zokrates, Snarky). These are now deployed in real-world systems. This talk will survey the state of the field, and focus on the need for formal methods in this area.
Michael Hicks - Contesting Secure Software Development
With the ongoing, frequent disclosure of the existence and exploitation of security vulnerabilities, one might wonder: How can we can build software that is more secure?
For decades, the CSF community has promoted software construction methodologies based on well-developed mathematical principles. While there is little doubt that such methodologies provide stronger assurances, they also come with non-trivial costs---developers may require re-training, software may take longer to construct or may be limited in scope, and system performance may suffer. How can we assess these costs vs. the benefits of security-minded development methodologies?
In an attempt to focus educational attention on this question, and gather empirical evidence at the same time, we developed the Build it, Break it, Fix it (BIBIFI) security-oriented programming contest. In BIBIFI, teams aim to build specified software that should be correct, efficient, and secure. Security is tested when teams attempt to break other teams’ submissions. Winners are chosen from among the best builders and the best breakers. BIBIFI was designed to be open-ended — teams can use any language, tool, process, etc. that they like.
We ran three 6-week contests involving a total of 156 teams from across the world, and three different programming problems. Most participants had previous development experience and security education. Careful analysis of the submissions and outcomes from these contests found several interesting trends. For example, the most efficient build-it submissions used C/C++, but submissions coded in a statically-type safe language were 11× less likely to have a security flaw than C/C++ submissions. As another example, vulnerabilities arising from a misunderstanding of security concepts were far more common (84% of projects) than vulnerabilities due to simple mistakes (24%). Overall, our results have implications for improving secure-programming language choices, API designs, API documentation, vulnerability-finding tools, and security education.
This is joint work with James Parker, Andrew Ruef, Dan Votipka, Kelsey Fulton, Matthew Hou, Michelle Mazurek, and Dave Levin, all at the University of Maryland.
The following papers have been accepted to CSF 2020. The first three papers were selected for the Distinguished Paper award.