Deep Specifications in the Wild 2017DSW 2017
DeepSpec is a 5-year, 4-institution initiative to push forward the state of the art in applying computer proof assistants to verify realistic software and hardware stacks at scale. A key part of the mission is to engage with industry, learning about adoption obstacles, educating practitioners about how to apply these techniques, and even launching pilot collaborations with specific companies. For that reason, we want to bring together academics and industrial engineers to discuss the low-hanging fruit of particular formal tools that are ready for tech transfer.
What makes the proposed workshop different from a research conference is its focus on particular ideas and artifacts that industry should be able to start experimenting with in the next year or two. What makes the proposed workshop different from a developer conference is that we are willing to consider technology investments (in formal methods, in particular) that may take years to pay off, but which seem promising to deliver significant increases in assurance levels and/or significant decreases in development costs.
List of Presentations
A detailed schedule will appear soon, with more information on talks and speakers, but here is the plan as of now.
Invited Speakers from Industry
- Aleksey Nogin from HRL, on integrating formal-methods tools in the DARPA HACMS program
- Dominic Rizzo from Google, on applying proof assistants to cryptography at Google
- Michael Tautschnig from Amazon, on static analysis of hypervisor code
Speakers From the DeepSpec Project
While the industry speakers represent a variety of formal-methods approaches, the presentations from our team will all be about work done with the Coq proof assistant.
- Andrew W. Appel from Princeton, on verifying concurrent C programs with the Verified Software Toolchain
- Lennart Beringer from Princeton, on verifying cryptographic C code with the Verified Software Toolchain
- Adam Chlipala from MIT, on generating low-level cryptographic code automatically from specifications
- Zhong Shao from Yale, on verifying the CertiKOS hypervisor OS kernel
Presentations
A Day of Invited Talks
There is no call for contributions.
Thu 22 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 15mDay opening | Introduction to DeepSpec DSW | ||
09:15 45mTalk | Building Faith in Experts: Applying Formal Verification to Cryptography DSW Dominic Rizzo Google | ||
10:30 - 12:10 | Academic crypto projects; industry perspective on formal-methods integrationDSW at Vertex WS216 Chair(s): Zhong Shao Yale University | ||
10:30 30mTalk | Correct-by-Construction Generation of Fast Code for Elliptic Curves DSW Adam Chlipala Massachusetts Institute of Technology, USA | ||
11:00 30mTalk | Introduction to verification using the VST DSW Lennart Beringer Princeton University | ||
11:30 40mTalk | Using formal tools to develop high-assurance software for autonomous ground vehicles DSW Aleksey Nogin HRL Laboratories, LLC | ||
13:40 - 15:00 | Academic C-verification project; industry perspective on hypervisorsDSW at Vertex WS216 Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA | ||
13:40 40mTalk | Verifying concurrent C programs with the Verified Software Toolchain DSW Andrew W. Appel Princeton | ||
14:20 40mTalk | Challenges in Analysing Virtualisation Stacks DSW Michael Tautschnig Amazon Web Services | ||
15:30 - 17:00 | Academic hypervisor project; closing discussionDSW at Vertex WS216 Chair(s): Lennart Beringer Princeton University | ||
15:30 45mTalk | CertiKOS: A Breakthrough toward Hacker-Resistant Operating Systems DSW Zhong Shao Yale University | ||
16:15 45mDay closing | Closing discussion DSW | ||
| Thu 22 Jun 2017 - Workshop |
