USTC-Yale Joint Research Center for High-Confidence Software

Project RCAL86
 

Overview
 

Realistic Certifying Assembly Language (RCAL86) is a project funded by Intel.This project is to find an appoach for building safe and reliable software.We think the safety guarantee through program type-checking is not enough,because type can only encode simple program properties.So we choose the combination of logical reasoning system and type theory as the resolution.
We try to build certified memory management module of operating system in the framework of PCC(Proof Carrying Code).With the help of Coq, we'll first give the formal description of RCAL86,and then implement certified memory management module (buddy system and slab allocator) for a simplified but practical x86-like machine model to convince its expressiveness.

 
Project Goals
The main goal is to implement certified memory management module.In order to realize this goal,subgoals below are to be realized.

• Design a certifying language RCAL86,and give its formal description.
• Implement buddy system and slab allocator in RCAL86.
• Write program's specification,and construct the proof that programs satisfy specification with the help of Coq.
• Check the proof with Coq's proof-checker.If all the proofs are correct, the program written in RCAL86 is certified.
   

  Technology Overview
  We'll select a simplified subset of IA32 instruction set as RCAL86's instruction set. Beside this,RCAL86 also include a specification language to annotate the program.In order to reason about the program written in RCAL86,we should give the formal description about RCAL86's operational sematics ,machine model, program's well-formedness rule.
  We'll implement a simple memory management in RCAL86 (include program and its specification), Then we need to prove that program satisfies its specification.There are many other approaches to construct the proof,such as Boyer-Moore theorem prover,Elf.We prefer Coq because its semi-automatic mode can help proving more properties of program, and the specification language of Coq is more expressive.Specification of program is very large,we can reduce its size by assert macro.Size of proof is also large,we can reduce it by construct lemma library efficiently.
  Finally,we'll have the proof automatically checked to make sure that the proof is correct. After that, program can be extracted from the formal proof and the program has been certified.

   
  Status
  Certified Buddy System in RCAL86
  Certified Dynamic Storage Allocation in Stack Based CAP
  Bit-level Abstraction
  All Vernacular file can be compiled with coqc (command of Coq-8.0).
   
  Reference

• Automated Theorem Proving in a Simple Meta-Logic,CMU,Schurmann&Pfenning
• A Verified Operating System Kernel,UT Austin,Bevier
• Automated Proofs of Object Code ,UT Austin,Boyer
• Building Certified Libraries for PCC,Yale,Dachuan Yu
• Logical Reasoning Systems ,At&T Labs-Research,McAllester
• Proof-Carrying Code,CMU,Necula
• Proofs of Safety for Untrusted Code,UC San Diego,Rosu&Segerlind
• TAL for x86
• From System V to TAL
• Typed Machine Language and its semantics
• Foundational Proof Carrying Code
• Syntactic Approach For FPCC
• Safety Verification of Low-Level Code
• Reynolds:A logic for shared mutable data structure
• Hoare:A axiomatic basis for computer programs
• Harper:Programming language:theory and practice
   
  Documents
• A Real Certified Assembly Language(draft)
• rcal86-ch.pdf
• Proposal:Toward Building Trusted Systems
• Progress Status Report For Intel
  Using Coq
   
• Using Coq to Write Formal Description of RCAL86.
  Formalize instruction set:

  Inductive inst:Set:=
  add : reg->reg->reg->inst(*add rd,rs1,rs2*)
  |...............
  |...............
  .

  Formalize machine model:

  Inductive rfile:Set := nullrf:rfile
  |consrf:rfile->reg->int->rfile.
  Inductive stack:Set:=............................
  Inductive heap:Set:=.............................
  Definition state:=(rfile * stack * heap)%type.
  Definition program:=(codemap * cb * state)%type.
  (*program consists a codemap which maps label into code block,
  the program entry code block,and the initial machine state*)

  Formalize operational semantics:

  Inductive Eval : program->program->Prop :=
  |ev_add: .................
  .......................