Project RCAL86

Gnu/Linux Coq Gnome
Project RCAL86


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.