Isolation theorems of the framework:
- Preservation of the invariant: formalization/dma_framework/lemmas/l4/invariant_l4_preservationScript.sml:SYSTEM_PRESERVES_INVARIANT_L4_LEMMA
- Issued memory requests address readable and writable memory: formalization/dma_framework/lemmas/l4/memory_isolationScript.sml:DMA_READ_WRITE_LEMMA
Isolation theorems of the BBB USB instantiation:
- Preservation of the invariant: formalization/dma_framework/instantiations/bbb-usb/bbb_usb_isolationScript.sml:BBB_USB_PRESERVES_INVARIANT_L4_LEMMA
- Issued memory requests address readable and writable memory: formalization/dma_framework/instantiations/bbb-usb/bbb_usb_isolationScript.sml:BBB_USB_DMA_READ_WRITE_LEMMA
Compilation on an ubuntu distribution:
- Compilation of the framework: Go to formalization/dma_framework/lemmas/l4/ and type sh compile.sh in the terminal.
- Compilation of the BBB USB instantiation: Go to formalization/dma_framework/instantiations/bbb-usb/ and type sh compile.sh in the terminal.
The core files of the framework are:
- formalization/dma_framework/definitions/framework/stateScript.sml: The definitions of the data structures used in the framework, including comments for the functions to be instantiated.
- formalization/dma_framework/definitions/framework/operationsScript.sml: The definitions of the operations of the framework.
- formalization/dma_framework/definitions/framework/proof_obligationsScript.sml: The definitions of the proof obligations of the framework, including comments.
- formalization/dma_framework/lemmas/: Folders containing different types of lemmas, including the lemmas for each of the four abstraction layers.