Development of systems software—including device drivers, operating systems, microkernels, and hypervisors—is particularly challenging when high levels of assurance about program behavior are required. On the one hand, programmers must deal with intricate low-level and performance-critical details of hardware. On the other hand, to ensure correct behavior, including critical safety and security properties, the same code must also be related directly and precisely to high-level, abstract models that can be subjected to rigorous analysis, including mechanized formal methods. Failure of computer software can be a major problem in any application domain. However, the consequences of failure in systems software are especially severe because even simple errors or oversights—whether in handling low-level hardware correctly or in meeting the goals of high-level verification—can quickly compromise an entire system.
Functional programming technology can help achieve higher-assurance systems software. Most current systems software is built using fairly low-level languages and tools. By comparison, modern functional languages support much higher levels of program abstraction than have traditionally been possible in this domain. Using higher-level languages yields software engineering benefits in the form of increased productivity and opportunities for code re-use. Perhaps more importantly for high-assurance software, there are immediate benefits from using a type-safe and memory-safe language that prevents many potentially compromising errors. Finally, the use of a pure functional language—with strong, mathematically defined foundations—offers the possibility of supporting mechanized formal verification and validation of the software.
Our work to date has demonstrated that the pure, lazy functional language Haskell is indeed a promising platform for high-assurance systems programming. But it has also revealed vulnerabilities in the design and implementation of Haskell, and gaps in our tool set for formal reasoning about Haskell programs. The research proposed here aims to address these problems by defining and implementing a new language, a high-assurance run-time system for it (HARTS), and additional formal tools for reasoning about these.
Our experience with Haskell has revealed a number of significant vulnerabilities in using functional languages for systems software development.
Predicting and controlling resource usage.One of the great advantages of high-level languages is that they free programmer from many explicit concerns about resource management. For example, Haskell provides safe, implicit management of memory allocation and deallocation, via a garbage-collected heap. The GHC Haskell dialect also supports concurrent threads, which are implicitly allocated and scheduled (possibly over multiple processors) by the underlying run-time system. Finally, Haskell is a lazy language, so the programmer is not expected to worry about the order of execution, even within a single thread.
These features directly support programmer productivity, program safety, and reasoning about programs. Unfortunately, they also have a negative side: they make systems programming difficult. Systems programmers sometimes need to control resources explicitly in order to achieve performance goals or to access particular low-level machine features. But Haskell doesn't provide graceful mechanisms to shift between implicit and explicit resource management. Indeed, in the presence of lazy evaluation, programmers find it very difficult just to predict—let alone to control—space and time consumption.
Validating the run-time system.Another consequence of making resource control implicit in the language is the need for a underlying run-time system. Any assurance argument we might make about a program written in a functional language requires a corresponding argument about the run-time system.
Unfortunately, existing run-time systems are not designed for validation. For example, the run-time system (RTS) for GHC, currently the most widely-used implementation of Haskell, is large, complex and mostly written in C. Verifying the GHC RTS is not currently an option: Machine-based verification of non-trivial imperative pointer programs—such as a garbage collector—is only just now beginning to become a reality. On the other hand, writing an RTS in an existing high-level language is not practical. Such languages cannot express complex pointer manipulations, such as those needed for garbage collectors, without unduly compromising safety.
Realistic, mechanized formal verificationHaskell is a pure language that supports paper-and-pencil reasoning very well. Because of this, the Programatica project initially believed that it would be relatively simple to build mechanized tools for doing program proofs. But in practice, this task was difficult. Haskell is a large language with a complex semantics that had never been fully formalized before we started Programatica; we have (nearly) completed that task, but it has been a lengthy one. Moreover, we discovered substantial differences between the needs of semi-formal manual proofs and mechanized program verification.
Many language features are challenging to model precisely in current theorem provers. One notable example is Haskell's rich type system (with type constructors, GADTs, etc.) Another example is non-termination (which is even more pervasive in a lazy language than in an eager one). Both make it difficult to embed Haskell into a theorem prover like Isabelle/HOL or Coq, despite Haskell's superficial similarity.
We are also concerned that proving properties of Haskell source programs may not give us enough confidence in the corresponding executables. Any prospect of a formally validated compiler for a language as complex as full Haskell seems distant. Even informal validation methods, such as side-by-side comparison of source and target, are impractical for Haskell. Though these informal methods are widely used for lower-level languages like C, they are difficult to use for Haskell due to its complex compilation pipeline.
For more details, visit this page again or contact us.