13:30 - 15:00
Session 3[Workshop] HILT' 22
at Ballroom C East
- 1330-1530 Session #2 : Language and Assurance
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.
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.
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