forked from gangtan/CPUmodels
-
Notifications
You must be signed in to change notification settings - Fork 2
CertiKOS/CPUmodels
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
The Model and RockSalt directories last checked in Coq 8.5pl2 x86model/ A Coq formalization of x86-32 x86model/Model An x86-32 model (up to date to Coq 8.5) x86model/RockSalt A formally verified SFI checker based on our model of x86 (mostly up to date to Coq 8.5, except for NaclJmp and DFACorrectness; however, recent changes in x86Semantics.v made the proof broken; needs fix) x86model/fuzz A fuzz tester for the x86 model (sorry, but hasn't tested this for a while) x86model/cdriver A C implementation of an SFI checker using our certified DFAs (sorry, but hasn't tested this for a while) x86model/semantics_trace Simulation and instrumentation of x86 binaries (sorry, but hasn't tested this for a while) MIPSmodel/ A Coq formalization of a MIPS processor ------------------------------------------------------------ Installation: * How to build the CPU models? You will need Coq 8.5pl2. - install the ocaml package manager opam - opam repo add coq-released https://coq.inria.fr/opam/released - opam install coq-flocq-2.5.1 - For x86, go to x86model and type make - For MIPS, go to MIPSmodel and type make * How to build the validation tools? (sorry, haven't checked this for a while; it may not working) First, build the x86 CPU model. Then, you will need OCaml 3.12 (or a more recent verison), and pin (http://www.pintool.org/). Please go to the x86model/semantics_trace directory and for further instructions. * How to build the RockSalt C driver? (sorry, haven't checked this for a while; it may not working) You will need to install the developer version of native client first. Then, replace the native_client/src/trustaed/validator_x86/ncval.c file with ours, make sure the include for tables.h and driver.h are properly set, and build native client as usual. The resulting ncval binary can run RockSalt by passing the command line ragument --dfa. ------------------------------------------------------------ Todo list: - To be fixed: The Rocksalt directory is broken after changes to x86Semantics.v - To be fixed: in x86Semantics.v, the flags are set nondeterministically in SHL/SHR, although the manual doesn't say so
About
GoNative project: formal machines models in Coq
Resources
Stars
Watchers
Forks
Packages 0
No packages published
Languages
- OCaml 46.4%
- Coq 44.5%
- C 3.4%
- Objective-C 2.7%
- Standard ML 1.9%
- Assembly 0.6%
- Other 0.5%