Developer-Friendly Contract-Based Notations and Machine-Checkable Evidence for Verif. of Information Flow Properties for ES
Presented as part of the 2012 HCSS conference.
Abstract:
Network and embedded security devices including cross-domain solutions, network guards, and message routers have information flow policies that are complex and crucial to fulfilling device requirements. To be used in military and national infrastructure systems, such devices must often be certified to very stringent criteria such as Common Criteria EAL 6/7 and DCID 6/3. Past certification efforts have created models of software code in theorem provers and proved that the models of code comply with security policies – leaving “trust gaps” between source code and models and inhibiting developers from proceeding with verification during the development process.
To remove these trust gaps and to make information flow specification and checking more accessible to developers, it is desirable to have frameworks that support specification of information flow policies directly at the source code level as part of developer workflows. Spark, a subset of Ada for engineering safety and security-critical systems, is one of the best commercially available frameworks for formal-methods-supported development of critical software. Spark provides a source-level information flow specification and checking framework that has been used to support certification arguments on several different information assurance projects.
Our experience with Spark is derived, in part, from our collaborations with Rockwell Collins where Spark is used in security critical projects including the Janus high-speed cryptography engine and several other embedded information assurance devices. While SPARK provides information flow annotations and associated automated checking mechanisms, industrial experience has revealed that these annotations are not precise enough to specify many desired information flow policies. One key problem is that information assurance applications such as cross-domain solutions often contain information flow policies that are conditional in the sense that data is allowed to flow between system components only when the system satisfies certain state predicates. However, existing information flow specification and verification environments, including Spark, can only capture unconditional information flows. Another limitation of the Spark information flow framework is that arrays are treated as indivisible entities–flow that involve only particular locations of an array have to be abstracted into flow on the whole array. This has substantial practical impact since Spark does not allow dynamic allocation of memory, and hence makes heavy use of arrays to implement complex data structures.
In this talk, we will describe our experience in developing and applying a Hoare logic for information flow that enables precise compositional specification of conditional information flow policies in programs with arrays, and automated deduction algorithms for checking and inferring contracts in an enhanced SPARK information flow contract language that hides the details of the logic from the developer. To provide very high degrees of confidence, our algorithm for verifying code compliance to an information flow contract emits formal certificates of correctness that are checked in the Coq proof assistant. We demonstrate our techniques on a collection of simple information assurance examples.
Although the framework currently targets Spark, the techniques can be applied to other languages used for high-assurance applications such as safety critical subsets of C.
Biography:
Dr. John Hatcliff is a University Distinguished Professor at Kansas State University in the Computing and Information Sciences Department. His research areas include software engineering, formal methods, static analysis, security, software certification, and medical device development and integration. He has been a principal investigator on a number of DoD-funded projects from agencies such as the Air Force Office of Scientific Research, Army Research Office, and DARPA. His research has also been supported by the National Science Foundation, Lockheed Martin, Rockwell Collins, Intel, and IBM.