Sound Static Analysis for Security Workshop


Abstracts
Session 1: ANALYSIS OF LEGACY CODE
 

If it works, it’s legacy: analysis of legacy code

David A. Wheeler, Institute for Defense Analyses


Dr. Wheeler will provide an overview of how sound static analysis approaches can facilitate the development of higher quality and more secure versions of existing software. He will discuss the balance of risk and expense that must be considered when contemplating total redevelopment. Given, these systems can be: large, are not designed to be analyzed, and are often written in languages difficult to analyze, an engineering mindset, rather than a scientific or mathematical mindset is indicated. Examples of approaches that can help include: lightweight formal methods (which emphasize partial specification and focused application), sound analysis of high-level models (particularly of protocols), easing the combination of sound analysis with other approaches (e.g., strengthening tests, human review, and start-up checks), analysis of prevention/hardening/detection/response mechanisms, improving tools to handle scale and real constructs (not subset), providing useful feedback on "how to change the code to be analyzable," and improving the interactions between developers and makers of sound tools. Releasing sound analysis tools as open source software (OSS) enables users to improve the tools so that they be purposed or repurposed to a specific use. Perhaps most importantly, supporting incremental application greatly eases adoption and use.


Proving sequential properties of unmodified Linux kernel code
Alexey Khoroshilov, Linux Verification Center of ISPRAS


Verification of legacy code often means that you have no ability to fix the code to simplify its verification.As a result verification tools have to support many complex corner cases in semantics of the target programming platform, most notably in low-level platforms based on C programming language that lack well-defined semantics for many cases widely used in practice. The talk presents the experience in proving sequential properties of Linux kernel code using Frama-C with AstraVer plugin that has appeared as an attempt to solve this problem by implementing support for C code used in Linux kernel. The first target for the AstraVer plugin was a custom implementation of Linux security module that is a component responsible for implementation of access control policy. Another target was a set of unmodified Linux kernel library functions implementing conventional memory and string operations.


Proving security properties in software of unknown provenance
Ben Hocking, Dependable Computing


In the safety and security community, everyone knows that the best time to include formal analysis of your desired properties is at the very beginning. If formal methods are not involved during requirements analysis, or during the specifications phase, then at least one should apply formal methods during the implementation phase. However, what if one is using Software of Unknown Provenance (SOUP) after all of these phases have already passed? Has the safety/security "horse" already left the stable? Techniques used to ensure SOUP has desired properties include sandboxing and/or altering the binary code after the fact to catch potential violations of the properties one wishes to enforce. However, these approaches can add memory or latency overhead to the executable that might not be acceptable, especially for embedded systems. A model of the X86 architecture in SPARK Ada, along with a system for translating binaries into a SPARK Ada representation that uses this model, allows for the proof of these desired security properties. This enables binary modification to be limited to parts of the binary that cannot be proven to have the desired properties.


The Q-compiler for verifying high-consequence controls
Jon Aytac, Sandia National Labs


The purpose of the Q compiler is to prove relatively complexproperties about relatively simple digital controls -- controls for high-consequence systems where correctness is critical to safety. Starting with a generalized state machine, called a statechart, and progressing through multiple refinements, the state machine transition relation is proven against implementation code. The implementation can take the form of either C, using ACSL and Frama-C, or VHDL/Verilog using SVA in a commercial prover (e.g. Jasper). Refinements, and refinement across language boundaries afford a number of advantages. It enables proofs for more complex properties, more scalably than would otherwise be possible. The presentation will include some theory and an example of the development process.


Applying formal methods to existing software: what can you expect?
by Benjamin Monate, TrustInSoft


Formal methods-based source code verification tools have a very strong promise: mathematically prove that a piece of software is perfect. In some specific economic sectors, new languages have been adopted to help developers build perfect-by-construction software. But the vast majority of software is not perfect-by-construction and experience shows that it comes with tons of bugs. In this talk I will discuss what developers can expect from the application of formal methods-based tools to existing imperfect-by-construction code bases, what they should not expect, and how such tools will help make the software better and better by incrementally reducing its hidden technical debt. This work has been supported by the Core Infrastructure Initiative of the Linux foundation.


Session 2: USE IN NEW DEVELOPMENTS
 

Trends in automated verification

K. Rustan M. Leino, Amazon


Mechanized support for formally verifying programs has undergone dramatic improvements in the last couple of decades. Tools now offer more automation and are easier to use than ever before. The languages and specifications used as input to automated verifiers are also becoming more powerful and expressive. In this talk, I will give some history leading to the current state of automated verifiers, and will demonstrate some advanced applications of such tools.


Reimplement? Reuse? Both! - trustworthy systems with Genode and SPARK
Alexander Senier, Componolit


Formal verification is key to trustworthy systems. Especially when used for sensitive or critical applications. However, no matter which technology is used, the verification effort usually exceeds the costs for the actual implementation considerably. Hence, the verification of complex subsystems like device drivers, file systems or media codecs often is prohibitively expensive.
To improve on that situation for systems with confidentiality and integrity requirements, we realize component-based architectures based on the Genode OS framework. While we can reuse a lot of existing code, verified SPARK components maintain guarantees by wrapping, validating, sanitizing or resetting untrusted components. We present the different strategies and showcase their application to complex communication protocols using the example of the Componolit baseband filter. This SPARK component enables safe reuse of complex untrusted software by validating the interaction between Android and a radio communication processor.


Mixing formal methods to increase robustness against cyber-attacks
Laurent Voisin, Systerel


Already known as a specialist in applying formal methods for the development or the evaluation of safety critical systems, Systerel has recently expanded its usage of these mathematical technologies to cybersecurity. Its first concrete realisation is the production of a safe and secure open-source implementation of the OPC-UA protocol (available at https://s2opc.com). The OPC-UA protocol (IEC 62541) is dedicated to machine to machine communication and is a cornerstone of the Industry 4.0 initiative for smart manufacturing. By using concurrently two formal approaches, Systerel has reduced drastically the presence of specification and design flaws thanks to the B method, while code vulnerabilities have been eliminated with Frama-C and TrustInSoft Analyser. In this talk, we will present the rationale for the choice of using two different verification approaches and the advantages that they bring together.


Enhance verification using ghost code
Claire Dross, AdaCore


When using tool assistance to verify a software, users are generally faced with two equally complex challenges. How can I express my requirements in the supported language, and how can I convince the tool that my software indeed meets my requirements. Ghost code, or verification specific code, is a construct provided by several formal verification oriented languages to enhance verification. This talk will describe how ghost code can be used in SPARK to enhance both expressivity and provability. Different uses will be exemplified, ranging from simple instances, such as assertions and contracts, to more involved use cases, like model functions and lemma procedures.


A formally verified floating-point implementation of the Compact Position Reporting algorithm
Mariano M. Moscato, National Institute of Aerospace


The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate their current state, including position and velocity information, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting (CPR) algorithm is the ADS-B module responsible for the encoding and decoding of aircraft positions. CPR is highly sensitive to computer arithmetic since it heavily relies on functions that are intrinsically unstable such floor and modulo.
This talk reports on how Frama-C was used to verify that a double-precision implementation of CPR is correct with respect to its operational requirement. In this effort, Frama-C is used synergically with different kinds of provers such as Gappa, Alt-Ergo, and PVS. The verified algorithm is currently being considered for inclusion in the revised version of the ADS-B standards document as the reference implementation of the CPR algorithm.


Session 3: ACCOUNTABLE SOFTWARE QUALITY
 

Lessons from verify legacy Java code for C++ specification & verification

David Cok, Visiting Research Engineer at CEA and Independent Consultant


Legacy code is typically written with no regard for specification and verification. Consequently verification tools applied to legacy code must support most language features and be able to scale to the size and scope of industrial software. This talk will use case study examples from a verification project targeting industrial Java code to demonstrate both how verification of features in Java 8 was achieved and what challenges still remain for such projects. Then we will illustrate how the lessons learned from that project are informing the design of a specification language for C++.


Soundness, evidence and discipline in high-assurance software
Roderick Chapman, Protean Code Limited


This talk will reflect on the need for soundness in software verification, and (more generally) the issue of trust in automated verification tools. If a tool vendor says their tool is "Sound", should you believe them? What does this really mean in practice, and what assumptions underpin such claims? If you develop trust in a tool, what effect does this have on engineers' behaviour and engineering process? Finally, we'll consider what role soundness plays for security claims in the face of an overtly malicious environment.


Runtime verification of security properties with E-ACSL
Julien Signoles, CEA LIST, Software Security and Reliability Lab


Frama-C is a framework for code analysis of C code, including many analyzers. This talk presents E-ACSL, its runtime verification tool, and its applications to verification of security properties. E-ACSL automatically converts a C code annotated with formal specifications to another C code that checks them at runtime. Several usages of E-ACSL rely on automatic generation of these specifications, so that writing them by hand is not necessary. The verification process is therefore fully automatic. In this talk, we will focus on such automatic usages for verification of security properties, including verification of memory safety and information flow properties.


Industrial use of Formal Methods: a feedback from various experiments with Frama-C
David Mentré, Mitsubishi Electric R&D Centre Europe (MERCE)


Mitsubishi Electric is a worldwide group developing a wide range of business to business solutions, from railway systems to satellites, from electric sub-stations to automotive equipment. Most of those solutions need to build safety and security at their core. Therefore Mitsubishi Electric, like all similar industrial groups, is struggling to keep or improve the quality of its products while reducing costs and time-to-market. Formal Methods is more and more perceived as a viable approach to reach this objective, but applying Formal Methods is not an easy journey. In this presentation, we will show some of the needs appearing in domains like railway or automotive, and how we can address those needs using Frama-C and its plug-ins like Value Analysis, WP or PathCrawler, both in the short term and in the long term, giving along the way our feedback on those experiments.


Practical application of SPARK: a business case and roadmap for new users
Stuart Matthews, Altran


The range of options available when applying SPARK can be daunting for users who are new to the field of formal methods and static verification. More recently Altran UK have mapped our experience on previous projects into a framework (co-developed with AdaCore and Thales) which is intended to provide new users with a roadmap for navigating their way to obtaining optimum value from using SPARK. The details of how SPARK should be applied depends on multiple factors which include the required integrity level, applicable standards, and the overall verification strategy for the system. Far from being academic, theoretical or an idealistic vision, we demonstrate a highly pragmatic approach which is not only demonstrably beneficial but also accessible and practicable by developers who are new to the application of formal methods. As well as presenting the framework and its historical context, this talk will reflect on the wider business case and commercial implications for the application of SPARK within an organisation such as Altran which is responsible for delivering high integrity systems.


Proving memory safety of C programs
Henny Sipma, Kestrel Technology, LLC


Heartbleed demonstrated that lack of memory safety is still a problem. Bug finders have made large strides in recent years, but they are not exhaustive and memory corruptionn vulnerabilities continue to be exploited today at large scale. In this talk we present a mathematical approach for analyzing C source code that has the ability to provide full assurance for memory safety. The methodology takes the C standard as its specification and creates proof obligations that assert the necessary preconditions for safe execution for all language constructs that can lead to undefined behavior. Proofs of these proof obligations provide explicit and auditable evidence of full memory safety.
The methodology has been implemented in the KT Advance Analyzer and has been applied to more than a million lines of open-source C code. We discuss the challenges of the last mile in reaching 100% proof obligation discharge for legacy code, the opportunities for improving analyzability of new projects and the side benefits of enhanced maintainability and automatic generation of API documentation that the methodology offers.


Reflections on industrial use of Frama-C
Joe Kiniry, Galois


We reflect upon the use of Frama-C across multiple projects at Galois focused on mission-critical systems. In particular, we will focus on the opportunities and challenges in using several Frama-C plugins as compared to comparable tools for other platforms and programming languages. Topics we intend to cover include specification language expressiveness, tool robustness, assurance case strength, multi-tool coherence, and usability and comprehensibility by non-expert clients.



CEA List logo AdaCore logo NIST logo