A formalization in HOL4 of a machine independent language for defining the semantics of microarchitectural features such as out-of-order execution.
- License: BSD-3-Clause
- Related publications:
Requirements:
- Poly/ML 5.8.1 (or later)
- HOL4 kananaskis-14
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.
-
misc
: miscellaneous utility definitions and results, not tied to MILottLib.sml
: some general SML definitionsottScript.sml
: some general HOL4 definitionsmilPermutationScript.sml
: definitions and theorems about permutations of lists under arbitrary equivalence relationsmilUtilityScript.sml
: general definitions and theorems about lists, finite maps, and predicate sets
-
semantics
: core MIL definitions and metatheorymilScript.sml
: HOL4 definition of MIL syntax and IO and OoO semanticsmilSyntax.sml
: SML interface to the MIL syntax in HOL4milTracesScript.sml
: definitions and theorems about traces following a labeled step relation, and related definitions for MILmilSemanticsUtilityScript.sml
: utility definitions and results about MIL definitionsmilMetaScript.sml
: definition of well-formedness, and general results about MIL's semanticsmilInitializationScript.sml
: initialization of MIL resourcesmilReorderScript.sml
: definitions and theorems about reordering of MIL traces, including a theorem on memory consistency for the OoO and IO semanticsmilCompositionalScript.sml
: definitions and theorems on basic composition of MIL programsmilNoninterferenceScript.sml
: definitions and theorems related to conditional noninterferencemilLifeCycleOoOScript.sml
: instruction lifecycle state machine results for OoO semanticsmilExampleBisimulationScript.sml
: definitions and theorems related to bisimulations for MIL programs
-
executable
: executable functions related to MIL and their theorymilExecutableUtilityScript.sml
: definitions and correctness proofs for executable versions of semantic functionsmilExecutableTransitionScript.sml
: definitions and soundness proofs for executable step functions for the OoO and IO semanticsmilExecutableCompletenessScript.sml
: completeness for executable step functionsmilExecutableInitializationScript.sml
: executable functions for initializing MIL resourcesmilExecutableIOScript.sml
: instruction-by-instruction generation of MIL executionsmilExecutableIOTraceScript.sml
: instruction-by-instruction generation of MIL tracesmilExecutableIOCompletenessScript.sml
: completeness for generation of execution and tracesmilExecutableExamplesScript.sml
: definitions and results useful when executing MIL programsmilMaxExeTraceUtilityScript.sml
: definitions and results related to maximal terminating executions of MIL programsmilExecutableHelperScript.sml
: examples of using execution generation on MIL programsmilExecutableCompositionalScript.sml
: definitions and theorems on basic composition of executable MIL programs
-
examples
: MIL program examples and related resultsmilExampleMoveScript.sml
: example MIL program implementing a high-level move instructionmilMaxExeTraceExampleMoveScript.sml
: theorems for analysing the information leakage relation of ExampleMove by using the executable IO functions.milExampleAssignmentScript.sml
: example MIL program implementing a high-level assignmentmilMaxExeTraceExampleAssignmentScript.sml
: theorems for analysing the information leakage relation of ExampleAssignment by using the executable IO functions.milExampleConditionalScript.sml
: example MIL program implementing a high-level conditionalmilMaxExeTraceExampleConditionalScript.sml
: theorems for analysing the information leakage relation of ExampleConditional by using the executable IO functions.milExampleSpectreOOOScript.sml
: example MIL program describing a Spectre-style out-of-order vulnerabilitymilMaxExeTraceExampleSpectreOOOScript.sml
: theorems for analysing the information leakage relation of ExampleSpectreOOO by using the executable IO functions.milExampleLoopScript.sml
: example MIL program implementing a high-level loopmilExampleBranchEqualScript.sml
: program that does branch on equal, and analysis of its traces by executionmilExampleCopyEqualScript.sml
: program that does copy on equal, and analysis of its traces by execution
-
bir
: translation from BIR to MIL with examplesbir_to_milLib.sml
: translation SML librarybir_to_mil_test_basicScript.sml
: translation testbir_to_mil_test_castScript.sml
: translation testbir_to_mil_test_cjmpScript.sml
: translation testbir_to_mil_test_execScript.sml
: translation testbir_to_mil_test_nzcvScript.sml
: translation testbir_to_mil_test_obsScript.sml
: translation testbir_to_mil_test_execScript.sml
: translation testbir_to_mil_test_storeScript.sml
: translation testmilScamvExperiment0Script.sml
: translation test
-
cakeml
: proven refinement of executable functions to CakeML, and utility codemilCakeScript.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
-
semantics
milScript.sml
: datatypesres
,e
,i
,act
,obs
,l
,State
; functionssem_expr
,translate_val
,Completed
,addr_of
,str_may
,str_act
,sem_instr
; relationsout_of_order_step
,in_order_step
milTracesScript.sml
: relationstep_execution
; functionstrace
,commits
,step_invariant
milMetaScript.sml
: functionwell_formed_state
; theoremswell_formed_OoO_transition_well_formed
,OoO_transition_deterministic
,OoO_transitions_can_be_applied
,OoO_transitions_exist
milMetaIOScript.sml
: theoremIO_transition_deterministic
milReorderScript.sml
: theoremsOoO_IO_well_formed_memory_consistent
,IO_OoO_memory_consistent
-
executable
milExecutableIOScript.sml
: functionIO_bounded_execution
; theoremsIO_bounded_execution_out_of_order_step_sound
,IO_bounded_execution_in_order_step_sound
milExecutableIOTraceScript.sml
: functionIO_bounded_trace
; theoremsIO_bounded_trace_out_of_order_step_list_sound
,IO_bounded_trace_in_order_step_list_sound
-
cakeml
milCakeScript.sml
: functionsIO_bounded_execution_cake
,IO_bounded_trace_cake
milCakeProofScript.sml
: theoremsIO_bounded_execution_eq_cake
,IO_bounded_trace_eq_cake
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.
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).
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.
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.