MIL
A formalization in HOL4 of a machine independent language for defining the semantics of microarchitectural features such as out-of-order execution.
Building
Requirements:
The hol Makefile task, which assumes Holmake is available on the system, builds all core HOL4 theories (i.e., excluding examples and theories related to HolBA and CakeML):
make hol
This can take up to a few minutes on a modern machine.
Files
-
misc: miscellaneous utility definitions and results, not tied to MIL
-
semantics: core MIL definitions and metatheory
-
executable: executable functions related to MIL and their theory
-
examples: MIL program examples and related results
-
bir: translation from BIR to MIL with examples
-
cakeml: proven refinement of executable functions to CakeML, and utility code
milCakeScript.sml: CakeML friendly definitions of MIL executable functionsmilCakeProofScript.sml: proofs that CakeML friendly functions refine the original MIL executable functionsmilProgScript.sml: proof-producing translation of CakeML friendly definitions to CakeMLmil_to_MilprintLib.sml: direct pretty-printing of MIL abstract syntax to CakeML concrete syntax, for when the CakeML translator is too slow
Key definitions and results
-
semantics
milScript.sml: datatypes res, e, i, act, obs, l, State; functions sem_expr, translate_val, Completed, addr_of, str_may, str_act, sem_instr; relations out_of_order_step, in_order_stepmilTracesScript.sml: relation step_execution; functions trace, commits, step_invariantmilMetaScript.sml: function well_formed_state; theorems well_formed_OoO_transition_well_formed, OoO_transition_deterministic, OoO_transitions_can_be_applied, OoO_transitions_existmilMetaIOScript.sml: theorem IO_transition_deterministicmilReorderScript.sml: theorems OoO_IO_well_formed_memory_consistent, IO_OoO_memory_consistent
-
executable
milExecutableIOScript.sml: function IO_bounded_execution; theorems IO_bounded_execution_out_of_order_step_sound, IO_bounded_execution_in_order_step_soundmilExecutableIOTraceScript.sml: function IO_bounded_trace; theorems IO_bounded_trace_out_of_order_step_list_sound, IO_bounded_trace_in_order_step_list_sound
-
cakeml
milCakeScript.sml: functions IO_bounded_execution_cake, IO_bounded_trace_cakemilCakeProofScript.sml: theorems IO_bounded_execution_eq_cake, IO_bounded_trace_eq_cake
Analyzed MIL Programs
The directory examples contains definitions of MIL programs and corresponding information flow analysis theorems in HOL4. The theory for each example program has two parts:
milExample<Program>Script.sml: definition of the example and bisimulation proofmilMaxExeTraceExample<Program>Script.sml: generation of the information leakage relation for the example using the IO executor
To build all example theories, run the following command:
make examples
This can take around 15 minutes on a modern machine.
BIR-to-MIL Translator
The directory bir contains an (unverified) SML function that translates a BIR program to a MIL program, and some examples of using this function.
To build the translator, HolBA with the tag FMCAD2022_artifact must be present in a sibling directory named HolBA:
git clone https://github.com/kth-step/HolBA.git
cd HolBA
git checkout FMCAD2022_artifact
With the HolBA directory available as a sibling, the translator can be built by running:
make bir
This can take a few minutes on a modern machine (due to BIR and some long-running examples).
CakeML Library for MIL
The directory cakeml contains definitions and scripts for generating a (verified) CakeML library that can process MIL data and programs.
To build the library, CakeML with the tag v1469 must be present in a sibling directory named cakeml:
git clone https://github.com/CakeML/cakeml.git
cd cakeml
git checkout v1469
With the cakeml directory available as a sibling along with HolBA as above, the library can be built by running:
make cakeml
This can take more than an hour on a modern machine, due to that some key CakeML theories must be built.
Running code compiled by CakeML
For convenience, we pretty-printed the MIL CakeML code along with an example for trace generation in the file mil_reg_translate.cml in the cakeml directory. This file can be compiled and run as follows, on an x86-64 machine:
wget https://github.com/CakeML/cakeml/releases/download/v1469/cake-x64-64.tar.gz
tar xzvf cake-x64-64.tar.gz
cd cake-x64-64
cp path/to/MIL/cakeml/mil_reg_translate.cml .
make mil_reg_translate.cake
./mil_reg_translate.cake
On a modern machine, compilation can take a few minutes, but running the program should take
only a few milliseconds to output the following MIL trace:
[il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0,
il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4,
il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0,
il 0wx4, il 0wx0, il 0wx4]
In comparison, the HOL4 EVAL_TAC call that proves the equivalent theorem
ex_bir_prog_IO_bounded_trace_long in bir/bir_to_mil_test_basicScript.sml
can take up to a minute.
评论