tiancheng-luo / cpumodels Goto Github PK
View Code? Open in Web Editor NEWThis project forked from certikos/cpumodels
GoNative project: formal machines models in Coq
This project forked from certikos/cpumodels
GoNative project: formal machines models in Coq
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.