Guaranteeing run-time integrity of embedded system software is an open problem. Trade-offs between security and other priorities (e.g., cost or performance) are inherent and resolving them is both challenging and important. The proliferation of run-time attacks that introduce malicious code (e.g., by injection) into embedded devices has prompted a range of mitigation techniques. One popular approach is Remote Attestation (RA), whereby a trusted part (verifier) checks the current software state of an untrusted remote embedded device (prover). RA yields a timely authenticated snapshot of prover state that which verifier uses to decide whether an attack occurred.
Current RA schemes require verifier to explicitly initiate RA, based on some unclear criteria. Thus, in case of prover’s compromise, verifier only learns about it late, upon the next RA instance. While sufficient for compromise detection, some applications would benefit from a more proactive, prevention-based approach. To this end, we construct CASU: Compromise Avoidance via Secure Updates. CASU is an inexpensive hardware/software co-design enforcing: (i) run-time binary immutability, thus precluding any illegal software modification, and (ii) authenticated updates as the sole means of modifying software. In CASU, a successful RA instance serves as a proof of successful update, and continuous subsequent software integrity is implicit, due to the run-time immutability guarantee. This obviates the need for RA in between software updates and leads to unobtrusive integrity assurance with guarantees akin to those of prior RA techniques, with better overall performance
casu
├── application
│ └── simulation
├── evaluation
├── demo
├── msp_bin
├── openmsp430
│ ├── contraints_fpga
│ ├── fpga
│ ├── msp_core
│ ├── msp_memory
│ ├── msp_periph
│ └── simulation
├── scripts
│ ├── build
│ └── verif-tools
├── verification_specs
│ └── soundness_and_security_proofs
└── vrased
├── hw-mod
└── sw-att
└── hacl-c
Environment (processor and OS) used for development and verification: Intel i7-3770 Ubuntu 16.04.3 LTS
Dependencies on Ubuntu:
sudo apt-get install bison pkg-config gawk clang flex gcc-msp430 iverilog
cd scripts && make install
To run soundness and security proofs, install Spot: https://spot.lrde.epita.fr/install.html
To generate the Microcontroller program memory configuration containing CASU trusted software (SW-Att) and sample application (in application/main.c) code run:
cd scripts
make mem
To clean the built files run:
make clean
As a result of the build, two files pmem.mem and smem.mem should be created inside msp_bin directory:
-
pmem.mem program memory contents corresponding the application binaries
-
smem.mem contains SW-Att binaries.
Note: Latest Build tested using msp430-gcc (GCC) 4.6.3 2012-03-01
This is an example of how to Synthesize and prototype CASU using Basys3 FPGA and XILINX Vivado v2017.4 (64-bit) IDE for Linux
-
Vivado IDE is available to download at: https://www.xilinx.com/support/download.html
-
Basys3 Reference/Documentation is available at: https://reference.digilentinc.com/basys3/refmanual
1- Clone this repository;
2 - Follow the steps in "Building CASU Software" (above) to generate .mem files
2- Start Vivado. On the upper left select: File -> New Project
3- Follow the wizard, select a project name and location . In project type, select RTL Project and click Next.
4- In the "Add Sources" window, select Add Files and add all *.v and *.mem files contained in the following directories of this reposiroty:
openmsp430/fpga
openmsp430/msp_core
openmsp430/msp_memory
openmsp430/msp_periph
/vrased/hw-mod
/msp_bin
and select Next.
5- In the "Add Constraints" window, select add files and add the file
openmsp430/contraints_fpga/Basys-3-Master.xdc
and select Next.
Note: this file needs to be modified accordingly if you are running CASU in a different FPGA.
6- In the "Default Part" window select "Boards", search for Basys3, select it, and click Next.
Note: if you don't see Basys3 as an option you may need to download Basys3 to Vivado.
7- Select "Finish". This will conclude the creation of a Vivado Project for CASU.
Now we need to configure the project for systhesis.
8- In the PROJECT MANAGER "Sources" window, search for openMSP430_fpga (openMSP430_fpga.v) file, right click it and select "Set as Top". This will make openMSP430_fpga.v the top module in the project hierarchy. Now it's name should apear in bold letters.
9- In the same "Sources" window, search for openMSP430_defines.v file, right click it and select Set File Type and, from the dropdown menu select "Verilog Header".
Now we are ready to synthesize openmsp430 with CASU's hardware the following steps might take several minutes.
10- On the left menu of the PROJECT MANAGER click "Run Synthesis", select execution parameters (e.g, number of CPUs used for synthesis) according to your PC's capabilities.
11- If synthesis succeeds, you will be prompted with the next step. Select "Run Implementation" and wait a few more minutes (tipically ~3-10 minutes).
12- If implementation succeeds select "Generate Bitstream" in the following window. This will generate the configuration binary to step up the FPGA according to CASU hardware and software.
13- After the bitstream is generated, select "Open Hardware Manager", connect the FPGA to you computers USB port and click "Auto-Connect". Your FPGA should be now displayed on the hardware manager menu.
Note: if you don't see your FPGA after auto-connect you might need to download Basys3 drivers to your computer.
14- Right-click your FPGA and select "Program Device" to program the FPGA.
To simulate CASU using VIVADO sim-tools, continue following the instructions on [Running CASU on Vivado Simulation Tools].
Evaluation of CASU hardware overhead is located in:
evaluation/
In each file, line 34 and 37 show number of LUTs and Registers required.
After completing the steps 1-10 in [Creating a Vivado Project for CASU]:
1- In Vivado, click "Add Sources" (Alt-A), then select "Add or create simulation sources", click "Add Files", and select everything inside openmsp430/simulation.
2- Now, navigate "Sources" window in Vivado. Search for "tb_openMSP430_fpga", and In "Simulation Sources" tab, right-click "tb_openMSP430_fpga.v" and set its file type as top module.
3- Go back to Vivado window and in the "Flow Navigator" tab (on the left-most part of Vivado's window), click "Run Simulation", then "Run Behavioral Simulation".
4- On the newly opened simulation window, select a time span for your simulation to run (see times for each default test-case below) and the press "Shift+F2" to run.
5- In the green wave window you will see values for several signals.
This application does the following steps:
- It already has a new software to be updated in variable 'update_code', and the corresponding authentication token in variable 'signature.
- First it blinks an LED for 5 times (with an interval of 0.2 sec) and later calls CASU_Secure_Update with update_code and signature as arguments.
- CASU_Secure_Update copies the signature to 'SIG_RESP_ADDR' location and update_code to second half of PMEM (0xf000).
- Invokes CASU_entry to perform authentication of update_code and its subsequent installation.
- CASU exits via CASU_exit to the binary of the new software now at 0xf024.
- The new software blinks an LED for 10 times (with an interval of 0.5 sec).
- Finally, keep running in infinite loop.
Before even the application executes, CASU_entry is invoked after boot, to check the status flag (which is 0 in this case), and then jump to application.
- CASU entry at boot (0xA000):
- application calling the download routine for update (0xE0F4):
- CASU entry at secure update call (0xA000):
- New software verification (0xA1E4):
- CASU jump to the new software (0xF024):
- End of new software: infinite loop (0xF072):
cd scripts
make run
This command line simulation is the fastest option, but it will only print the contents of the microcontroller registers at each cycle. For more resourceful simulation follow "Running CASU on Vivado Simulation Tools" above.
First, we need to install the verification tools:
cd scripts
make install
To check HW-Mod against CASU properties using NuSMV run:
make verify
CASU properties (along with VRASED ones) are in:
verification_specs/ltl_specs.smv