Subproject 2: Academic System

As a part of the Verisoft project, a pervasively verified system (the academic system) for writing, signing, and sending emails is to be constructed. As such, the academic system represents a vertical cross section of a real general-purpose computer system, covering all layers from the gate-level hardware description to communicating concurrent programs. The properties of the academic system correspond to the required standards for real systems. We describe the components of the academic system in bottom-up fashion.
Verisoft Email System

Processor Hardware

The hardware platform in Subproject 2 is given by the VAMP (Verified Architecture Microprocessor) [2]. The VAMP is a 32-bit RISC CPU with full DLX-instruction set including a set of IEEE-compliant floating point instructions, delayed PC, address translation, and support for maskable nested precise interrupts.

The VAMP hardware consists of a 5-stage pipeline with an out-of order Tomasulo scheduler with reorder buffer [3]. There are five execution units, the XPU, the MU (Memory Unit), and three FPUs (Floating Point Units). Instructions have up to six 32-bit source operands and deliver up to four 32-bit results. The floating-point units [4] are fully IEEE compliant and support single and double precision operations as well as denormal numbers and the full set of IEEE exceptions in hardware. The FPUs are pipelined and the multiplicative FPU has a cycle in the pipeline structure in order to compute quotients with Newton-Raphson iteration. The memory interface [5] of the VAMP consists of two MMUs (Memory Management Units) that access instruction and data cache, respectively, which in turn access a physical memory via a bus protocol. The caches support write-back and are kept consistent with snooping.

The formal verification of the VAMP with MMUs is finished.u The PVS sources of the full proof without MMUs are available here. The correctness arguments of the virtual memory of a hardware/software system are given in [6,7,8].

Compiler

We implement and formally verify a compiler based on a small-step semantics for C0, our restricted version of C. The implementation of the compiler has been done in C0. The proof needs to be based on small step semantics in order to allow for concurrent program execution and communication between programs. A correctness proof of a C0 compiler with big step semantics is given in the lecture notes [10, p. 72-94] of Professor Paul. An overview of a paper and pencil proof of the correctness of an operating system microkernel including compiler correctness is given in the following slides [9].

The specification of the C0 compiler in Isabelle/HOL and its implementation in C0 have been completed. We have proven formally with help of a Hoare logic for C0 that the implementation generates the same assembly code as the compiler specification. The proof that the generated assembly program simulates the original C0 program has been done on paper-and-pencil. Currently, the formal verification of this simulation theorem is in progress.

Microkernel and CVM Layer

The layer of communicating virtual machines (CVM), its implementation, and correctness proof is introduced in [11]. The CVM layer establishes a hardware-independent programming interface for a microkernel and a virtual computation environment for concurrently running processes. Some parts of CVM must be implemented in assembler since C0, a subset of regular C, lacks—for good reason—low-level programming constructs. The microkernel is based on the CVM interface and contains no assembler parts.

The microkernel is implemented in C0. The formal verification is in progress.

Operating System

The kernel calls of the above microkernel are targeted for the implementation of a simple operating system (SOS) on top of this. It offers file I/O, inter-process communication, remote procedure calls and access to the peripherals as system calls to user processes.

Networking and Communication Protocols

TCP/IP

The standard protocols Internet Protocol (IP, RFC 791), which provides packet-oriented communication, and Transport Control Protocol (TCP, RFC 793), which provides reliable connection-based communication are implemented.

The protocol standard has been formalised, as well as its relevant properties (liveness, safety, ordering of packets). Some of these properties have already been verified.

Mail Server (SMTP)

The mail server implements the Simple Mail Transfer Protocol (SMTP, RFC 2821). It provides the functionality for sending emails via SMTP (sendmail functionality), and it receives emails via SMTP and delivers them to the correct recipient/user (mail server functionality).

The SMTP protocol has been formally specified and implemented. The formal verification is in progress.

Application Software

Signature Module

This module provides the functionality for signing texts (in particular emails) and for checking such signatures. It uses an asymmetric signature algorithm (RSA-PPS) with an SHA hash function.

So far, there is a formal specification of the module's interfaces and of RSA-PSS (incl. error handling). RSA and SHA-1 have been implemented in C0, and a basic version of RSA has been verified.

Email Client

So far, the Email Client is the top-layer application and provides the user interface for the whole Academic System. It provides functionality for editing, signing, and sending emails, as well as receiving, checking the signature of, and reading emails.

The email client has been formally specified and implemented in C0. Its verification is in progress. Work on how to formally define security requirements of user interfaces (such as the email client) has been published in [1].

References

  1. Bernhard Beckert and Gerd Beuster. Formal Specification of Security-relevant Properties of User Interfaces. In Proceedings, 3rd International Workshop on Critical Systems Development with UML, Lisbon, Portugal. October 11-15, 2004.
  2. Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, and Wolfgang J. Paul. Instantiating uninterpreted functional units and memory system: functional verification of the VAMP. In CHARME 2003, volume 2860 of LNCS, pages 51-65. Springer, 2003.
  3. Daniel Kröning. Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University, Saarbrücken, Germany, 2001.
  4. Christian Jacobi. Formal Verification of a Fully IEEE-compliant Floating-Point Unit. PhD thesis, Saarland University, Saarbrücken, Germany, 2002.
  5. Sven Beyer. Putting it all together - Formal Verification of the VAMP. PhD thesis, Saarland University, Saarbrücken, Germany, 2005.
  6. Mark Hillebrand and Wolfgang J. Paul. Virtual Memory Simulation Theorems. Slides, 2003.
  7. Iakov Dalinger, Mark Hillebrand, and Wolfgang J. Paul. On the Verification of Memory Management Mechanisms. Technical Report, 2005.
  8. Mark Hillebrand. Address Spaces and Virtual Memory: Specification, Implementation, and Correctness. PhD thesis, Saarland University, Saarbrücken, Germany, 2005.
  9. Wolfgang J. Paul, Mauro Gargano, Mark Hillebrand, and Dirk Leinenbach. Correctness of an Operating System Microkernel. Slides, 2004.
  10. Wolfgang J. Paul, Dilyana Dimova, and Mario Mancino. Systemarchitektur (German). Lecture notes, Sommersemester 2002.
  11. Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, and Wolfgang Paul. On the Correctness of Operating System Kernels. In Proceedings, 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), Oxford, United Kingdom. August 22-25, 2005.

 
Revision 14 Dec 2006