Generating Proof-Carrying Code for the UDP protocol
Presented as part of the 2014 HCSS conference.
Abstract:
The security of modern systems increasingly depends on securing their internal and external communications. We present a case study in the automated generation of proof-carrying code for a common communication protocol (UDP). The specification of the protocol is expressed in terms of trace predicates that capture both normal-case processing and the various errors that can arise and how to handle them. The disjunction of the trace predicates covers the specified behaviors of the protocol. The trace predicates are expressed in a mixed algebraic/coalgebraic style of specification in the Metaslang language of Kestrel's Specware system. A derivation script is written manually that specifies a sequence of transformations from Specware's library. Specware executes the derivation script automatically with the effect of incrementally refining the initial specification into idiomatic C code that runs in the Linux kernel.
A key part of this ongoing effort has been to instrument each transformation to emit a proof of the correctness of the refinement that it effects. To date, we can generate proofs for the first half of the transformation sequence. The proofs are expressed in the ISAR format of the Isabelle proof system, enabling Isabelle to automatically check them. In other words, our approach is to automatically and simultaneously generate both the code and proof. There is no need for post-hoc verification. The design information that is applied by a specification transformation is instantiated to produce both a refined specification and the logical justification of the refinement step.
Presenter Bio:
Dr. Douglas R. Smith is Principal Scientist at Kestrel Institute, and President of Kestrel Technology LLC. He is a Fellow of the American Association of Artificial Intelligence (AAAI) and an ASE Fellow (Automated Software Engineering). He taught an advanced graduate course on knowledge-based software development at Stanford University during 1986-2000. Dr. Smith was Chairman of IFIP Working Group 2.1 on Algorithmic Languages and Calculi from 1994-2000.
His main research interest has been mechanizing the development of software from formal specifications. He is mainly responsible for the development of KIDS (Kestrel Interactive Development System), which has been used to synthesize many algorithms, including a variety of complex high-performance scheduling applications for the US Air Force. Theoretical developments arising from experience with KIDS were a key motivation for building theSpecware, Designware, and Planware systems. His current research focuses on automating system design, including the automatic enforcement of cross-cutting safety and security policies, and system code generation from formalized design patterns and software architectures.
Dr. Smith has over 30 years experience in the field of automated program synthesis and has published over 75 papers (see the CiteSeer surveys of most cited papers in Software Engineering and most cited authors in Computer Science). He has one patent. He received the Ph.D. in Computer Science from Duke University in 1979.