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.
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
monitordirectory), and a formally verified implementation (in theverifieddirectory). 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 anioctlinterface 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).
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.mdfor the generic, instructions.)- Install
scons,fsharp,nugetandmono-develpackages cd tools/valenuget 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_KERNELto point to it. -
Run
makein 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 installto copy the blob toINSTALLDIRin preparation for booting on a Pi, ormake qemuto 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
KERNELDIRpoints to the root of that directory, and runmake -C driverto 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-linuxande2toolspackages available, you can try settingGUEST_DISKIMGto point to the unmodified Raspbian image and then runningmake guestdisk/guestdisk.imgto (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/modprobeto execute its functionality.
To just run verification:
- There's a top-level Makefile target
make verifiedwhich verifies and (if verification succeeds) prints the code for the verified monitor. This also runs verification of noninterference properties (Dafny files underverified/secprop).
Komodo is licensed under the MIT license included in the LICENSE.txt file.
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 [email protected] with any additional questions or comments.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent