[Workshop] HILT' 22 -- Supporting a Rigorous Approach to Software DevelopmentASE 2022

• 830-840 Opening, S. Tucker Taft and Jerome Hugues

• 840-940 Keynote#1 : Rustan Leino, Senior Principal Engineer, Amazon Web Services

  Title Recent experience with developing formally verified software

  Abstract: Numerous impressive projects have developed formally verified software. Typically, the participants in such projects have been formal-methods experts. Can verification tools also be used by common software engineers? I will reflect on this question in the context of the most recent AWS Encryption SDK, a verified library developed in a team with no particular background in verification. I will also give an overview of the verification-aware programming language Dafny, which was used in this development.

  Bio: K. Rustan M. Leino is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services. Throughout his career, he has developed and applied tools for the formal verification of software. The most recent of these is the Dafny language and verifier, which has been used in projects and education for more than a decade. Leino is an ACM Fellow and a recipient of the CAV Award.

• 940-1010 Session #1: Formal methods and applications (part 1)
  1. Daniel Larraz (The University of Iowa) and Cesare Tinelli (The University of Iowa).

     Title: Finding Locally Smallest Cut Sets using Max-SMT.

     Abstract: Model-based development (MBD) is increasingly being used for system-level development of safety-critical systems. This approach allows safety engineers to leverage the resultant system model created in the MBD process to assess the system’s resilience to component failure. In particular, one fundamental activity is the identification of minimal cut sets (MCSs), i.e, minimal sets of faults that lead to the violation of a safety requirement. Although the construction of a formal system model enables safety engineers to automate the generation process of MCSs, this is usually a computationally expensive task for complex systems. In this paper, we present a method that leverages Max-SMT solvers to efficiently obtain a small set of faults based on a local optimization of the cut set cardinality. Initial experimental results show the effectiveness of the method in generating cut sets that are close or equal to globally optimal solutions (smallest cut sets) while providing an answer 5.6 times faster on average than the standard method to find a smallest cut set.

• 1030-1130 Session #1: Formal methods and applications (part 2)

  1. Daniel Larraz (The University of Iowa), Arjun Viswanathan (The University of Iowa), Mickaël Laurent (Université de Paris) and Cesare Tinelli (The University of Iowa).

     Title: Beyond model checking of idealized Lustre in Kind 2.

     Abstract: This paper describes several new features of the open-source model checker Kind 2. Its input language and model checking engines have been extended to allow users to model and reason about systems with machine integers. In addition, Kind 2 can now provide traceability information between specification and design elements, which can be used for several purposes, including assessing the quality of a system specification, tracking the safety impact of model changes, and analyzing the tolerance and resilience of a system against faults or cyber-attacks. Finally, Kind 2 is also able to check whether a component contract is realizable or not, and provide a deadlocking computation and a set of conflicting guarantees when the contract is unrealizable.

  2. Danielle Stewart (University of Minnesota) and John Hatcliff (Kansas State University).

     Title: An AADL Contract Language Supporting Integrated Model- and Code-Level Verification.

     Abstract Model-based systems engineering approaches support the early adoption of a model – a collection of abstractions – of the system under development. The system model can be augmented with key properties of the system including formal specifications of system behavior that codify portions of system and unit-level requirements. There are obvious gaps between the model with formally specified behavior and the deployed system. Previous work on component contract languages has shown how behavior can be specified in models defined using the Architecture Analysis and Design Language (AADL) – a SAE International standard (AS5506C). That work demonstrated the effectiveness of model-level formal methods specification and verification but did not provide a strong and direct connection to system implementations developed using conventional programming languages. In particular, there was no refinement of model-level contracts to programming language-level contracts nor a framework for formally verifying that program code conforms to model-level behavioral specifications. To address these gaps and to enable the practical application of model-contract languages for verification of deployed high-integrity systems, this paper describes the design of GUMBO AADL contract language that integrates and extends key concepts from earlier contract languages. The GUMBO contract language (GCL) is closely aligned to a formal semantics of the AADL run-time framework, which provides a platform- and language-independent specification of AADL semantics. We have enhanced the HAMR AADL code generation framework to translate model-level contracts to programming language-level contracts in the Slang high-integrity language. We demonstrate how the Logika verification tool can automatically verify that Slang-based AADL component implementations conform to contracts, both at the code-level and model-level. Slang-based implementations of AADL systems can be executed directly or compiled to C for deployments on Linux or the seL4 verified microkernel.

• 1130-1230 Keynote #2: Niko Matsakis, Senior Principal Engineer, Amazon Web Services

  Title: a-mir-formality: a formal model for the Rust language

  Bio: Nicholas Matsakis is a Senior Principal Engineer at AWS and co-lead of the open source Rust language design team. He has worked on Rust since 2011, and led the design of its “secret sauce”, the borrow checker. He has played a number of other roles in Rust over the years, such as being a member of the Rust core team, the lead of the Rust compiler team, and helping to launch the Rust Foundation. Prior to working on Rust, he completed a PhD at ETH Zurich and did his undergraduate study at MIT.

• 1330-1530 Session #2 : Language and Assurance

  1. David Hardin (Collins Aerospace).

     Title: Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero Trust Architecture Development.

     Abstract: Zero Trust Architecture requirements are of increasing importance in critical systems development. Zero trust tenets hold that no implicit trust be granted to assets based on their physical or network location. Zero Trust development focuses on authentication, authorization, and shrinking implicit trust zones to the most granular level possible, while maintaining availability and minimizing authentication latency. Performant, high-assurance cryptographic primitives are thus central to successfully realizing a Zero Trust Architecture. The Rust programming language has garnered significant interest and use as a modern, type-safe, memory-safe, and potentially formally analyzable programming language. Our interest in Rust particularly stems from its potential as a hardware/software co-assurance language for developing Zero Trust Architectures. We describe a novel environment enabling Rust to be used as a High-Level Synthesis (HLS) language, suitable for secure and performant Zero Trust application development. Many incumbent HLS languages are a subset of C, and inherit many of the well-known security shortcomings of that language. A Rust-based HLS brings a single modern, type-safe, memory-safe, high-assurance development language for both hardware and software. To study the benefits of this approach, we crafted a Rust HLS subset, and developed a frontend to the hardware/software co-assurance toolchain due to Russinoff and colleagues at Arm, used primarily for floating-point hardware formal verification. This allows us to leverage a number of existing hardware/software co-assurance tools with a minimum investment of time and effort. In this paper, we describe our Rust subset, detail our prototype toolchain, and describe the implementation, performance analysis, formal verification and validation of representative Zero Trust algorithms and data structures written in Rust, emphasizing cryptographic primitives and common data structures.

  2. Claire Dross (AdaCore).

     Title: Containers for Specification in SPARK.

     Abstract: The SPARK tool performs static analysis of Ada programs. It can be used to verify both that a program is free from runtime exceptions and that it conforms to a specification expressed through contracts. To facilitate dynamic analysis, Ada contracts are regular expressions which can be evaluated at execution. As a result, the annotation language of the SPARK tool is restricted to executable constructs. In this context, high-level concepts necessary for specification by contracts need to be supplied as libraries. For example, the latest version of the Ada language introduces unbounded integers and rational numbers to the standard library. In this article, we present the functional containers library which provides collections suitable for use in specification. We explain how they can be used to specify and verify complex programs through concrete examples that have been developed over many years.

  3. S. Tucker Taft (AdaCore).

     Title: Rigorous Pattern Matching as a Language Feature.

     Abstract: Structural pattern-matching as a language feature has become more common in programming languages over the past decade. This paper will consider more generally the challenge of adding pattern matching as a programming language feature, from the points of view of language design, rigorous static error detection, and effectiveness. In this context, a pattern matching language feature can be seen as providing a more rigorous approach to handling the complex conditionals that arise in processing highly structured input

• 1530-1700 Session #3 : Use Cases

  1. Tabea Bordis (Karlsruhe Institute of Technology), Tobias Runge (Karlsruhe Institute of Technology), Alexander Kittelmann (Karlsruhe Institute of Technology) and Ina Schaefer (Karlsruhe Institute of Technology).

     Title: Correctness-by-Construction: An Overview of the CorC Ecosystem (Short Abstract).

     Abstract: Correctness-by-Construction (CbC) is an incremental software development technique in the field of formal methods to create functionally correct programs guided by a specification. In contrast to post-hoc verification, where the specification and verification takes part after implementing a program, with CbC the specification is defined first, and then the program is successively created using a small set of refinement rules that define side conditions preserving the correctness of the program. This specification-first, refinement-based approach as pursued by CbC has the advantage that errors are likely to be detected earlier in the design process and can be tracked more easily. Even though the idea of CbC emerged over 40 years ago, CbC is not widespread and mostly used to create small algorithms. We believe in the idea of CbC and envision a scaled CbC approach that contributes to solving problems of modern software verification. In this short paper, we give an overview on our research regarding CbC in four different lines of research. For all of them, we provide tool support building the CorC ecosystem that even further enables CbC-based development for different fields of application and size of software systems. Furthermore, we give an outlook on future work that extends on our concepts for CbC.

  2. Laura Humphrey (Air Force Research Laboratory).

     Title: Basic Formal Verification of a Waypoint Manager for Unmanned Air Vehicles in SPARK.

     Abstract: As software becomes more complex, it becomes more difficult to verify its correctness. This poses a particular challenge for autonomous systems, since they are software-intensive and also require strong evidence of correctness in order to be allowed operate in real-world environments. One way to help address this problem is through the use of formal methods, i.e. mathematically-based tools for software and hardware verification. In this paper, we perform formal program verification on a service in OpenUxAS, a free and open source software framework for mission-level, multi-vehicle autonomy. More specifically, we apply the SPARK language and verification toolset to a service that sanity-checks and segments long sequences of vehicle waypoints to prove that it is free of runtime errors.

  3. Howard Ausden (Leidos).

     Title: Getting to 100% availability in a large C++ and Ada program.

     Abstract: Fault tolerance is a key requirement for air traffic control systems. A system failure could lead to hundreds of flights being delayed or cancelled. Using experience from earlier systems a set of techniques were built into our system at inception, including hot standby copies of executables and latest state checkpointed in disk files. As the system matured through formal testing and early site experience additional techniques were added to bolster the MTBF. These include exception safety, runaway process protection, and pro-active monitoring of the system to let us find and fix defects, often without the air traffic controllers being aware. Leidos now has a variety of techniques with defense in depth, and for new developments we scale the number of layers to the difficulty and impact of failure and recovery from the failure. Since Fall 2016, the customer has measured the system as 100% available at all operational sites.

1700 - 1715 Conclusion