Awesome
Project Komodo
Komodo is a research project that implements an SGX-like enclave protection model in formally-verified privileged software, for an ARMv7 TrustZone environment.
Note: this project is not maintained. This repository serves as a complement to the research paper:
Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP '17). 2017. ACM.
Components
Komodo consists of a number of different components:
-
A minimal Raspberry Pi bootloader (
piloader
) which loads the monitor in secure world, and then boots an existing OS image (typically Linux) in normal world. -
A secure-world monitor program which implements the Komodo protection model. There are two implementations: an early, unverified C/assembly implementation (in the
monitor
directory), and a formally verified implementation (in theverified
directory). The verified implemetnation is built and linked by default. -
A Linux kernel driver (
driver
) which interacts with the monitor using secure monitor calls (SMCs). In the future, it should implement anioctl
interface for user applications to create and execute protected regions, but at present it contains hard-coded test code.
The loader, monitor and kernel are all linked together into a single bootable
image (piimage/piimage.img
).
Building
Komodo builds on a Linux-like environment, which includes Cygwin and Windows Subsystem for Linux (WSL).
Required tools:
-
GNU make
-
An ARM EABI cross-compiler (gcc and binutils), such as this Linaro toolchain
-
Dafny, Boogie and Z3, which are provided as binaries under tools/dafny
-
Vale, which is tracked via a git submodule:
- Run
git submodule init && git submodule update
- Build Vale, making sure to point it at the correct copy of Dafny. (See
tools/vale/INSTALL.md
for the generic, instructions.)- Install
scons
,fsharp
,nuget
andmono-devel
packages cd tools/vale
nuget restore ./tools/Vale/src/packages.config -PackagesDirectory tools/FsLexYacc
- Build the vale tool with
scons --DAFNYPATH=$PWD/../dafny bin/vale.exe
- Install
- Run
The supported platform is currently Raspberry Pi 2, either a real board, or a custom QEMU, available from this GitHub branch.
To build komodo (loader, monitor, and Linux driver):
-
Adjust your environment to taste (e.g. create/edit config.mk and set the variables at the top of the Makefile)
-
Obtain a suitable Linux kernel image (e.g. from Raspbian), and set
GUEST_KERNEL
to point to it. -
Run
make
in the top-level directory. Assuming all goes well, this will verify and build the monitor, build the loader, then combine them with the kernel image to create a new bootable blob. -
You can use either
make install
to copy the blob toINSTALLDIR
in preparation for booting on a Pi, ormake qemu
to try booting it in QEMU (e.g. the version linked above). -
To build the Linux driver, you'll need the matching kernel sources and config for your Linux image. See here for some basic guidelines. Then make sure that
KERNELDIR
points to the root of that directory, and runmake -C driver
to build the driver. -
To get the Linux module loaded, you'll need a Linux disk image that includes the driver (
driver/komodo.ko
). If you have theutil-linux
ande2tools
packages available, you can try settingGUEST_DISKIMG
to point to the unmodified Raspbian image and then runningmake guestdisk/guestdisk.img
to (slowly!) copy the driver into place. Faster alternatives include mounting the image as a loopback device and copying the driver over manually. -
At present the driver includes a self-contained test enclave, and must be manually loaded via
insmod
/modprobe
to execute its functionality.
To just run verification:
- There's a top-level Makefile target
make verified
which verifies and (if verification succeeds) prints the code for the verified monitor. This also runs verification of noninterference properties (Dafny files underverified/secprop
).
License
Komodo is licensed under the MIT license included in the LICENSE.txt
file.
Contributing
This project welcomes contributions and suggestions. Most contributions require you to agree to a Contributor License Agreement (CLA) declaring that you have the right to, and actually do, grant us the rights to use your contribution. For details, visit https://cla.microsoft.com.
When you submit a pull request, a CLA-bot will automatically determine whether you need to provide a CLA and decorate the PR appropriately (e.g., label, comment). Simply follow the instructions provided by the bot. You will only need to do this once across all repos using our CLA.
This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact opencode@microsoft.com with any additional questions or comments.