EILID Paper (DATE'25) - arXiv
Prior research yielded many techniques to mitigate software compromise for low-end Internet of Things (IoT) devices. Some of them detect software modifications via remote attestation and similar services, while others preventatively ensure software (static) integrity. However, achieving run-time (dynamic) security, e.g., control-flow integrity (CFI), remains a challenge.
Control-flow attestation (CFA) is one approach that minimizes the burden on devices. However, CFA is not a real-time countermeasure against run-time attacks since it requires communication with a verifying entity. This poses significant risks if safety- or time-critical tasks have memory vulnerabilities.
To address this issue, we construct EILID – a hybrid architecture that ensures software execution integrity by actively monitoring control-flow violations on low-end devices. EILID is built atop CASU, a prevention-based (i.e., active) hybrid Root-of-Trust (RoT) that guarantees software immutability. EILID achieves fine-grained backward-edge and function-level forward-edge CFI via semi-automatic code instrumentation and a secure shadow stack.
eilid
├── cfi
│ └── instrumentation
├── eilid
│ ├── hw-mod
│ └── sw-att
│ └── hacl-c
├── examples
│ ├── charlieswitch
│ ├── firesensor
│ ├── lcd
│ ├── lightsensor
│ ├── syringepump
│ ├── tempsensor
│ └── ultrasonic
├── msp_bin
├── openmsp430
│ ├── contraints_fpga
│ ├── fpga
│ ├── msp_core
│ ├── msp_memory
│ ├── msp_periph
│ └── simulation
├── scripts
│ ├── build
│ └── verif-tools
├── secure_update
├── simulation
├── utils
└── verification_specs
└── soundness_and_security_proofs
Environment (processor and OS) used for development and verification: Intel i5-11400 Ubuntu 22.04.3 LTS
Dependencies on Ubuntu:
sudo apt-get install bison pkg-config gawk clang flex gcc-msp430 iverilog gzip tcl
cd scripts && make install
To run soundness and security proofs, install Spot: https://spot.lrde.epita.fr/install.html
If an error happens as below, you may need to set 'sh' to point to 'bash', not 'dash'.
build.sh: 24: [: Linux: unexpected operator
sudo rm /bin/sh; sudo ln -n bash /bin/sh
For fair evaluations, EILID has 7 sample applications from different public repositories.
To generate the Microcontroller program memory configuration containing EILID authorized software (SW-Att) and sample application (in example directory) code run:
cd script
make [charlieswitch/firesensor/lcd/lightsensor/syringepump/tempsensor/ultrasonic]
For example, to build firesensor,
make firesensor
in script directory.
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
Instrumented assembly is also generated as below,
scripts/tmp-build/app_instr.s
This assembly file is used to generate the binary.
This is an example of how to Synthesize and prototype EILID 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 EILID Software" (above) to generate .mem files
3- Start Vivado. On the upper left select: File -> New Project
4- Follow the wizard, select a project name and location . In project type, select RTL Project and click Next.
5- 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
/eilid/hw-mod
/msp_bin
and select Next.
6- 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 EILID in a different FPGA.
7- 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.
8- Select "Finish". This will conclude the creation of a Vivado Project for EILID.
Now we need to configure the project for systhesis.
9- 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.
10- 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 EILID's hardware the following steps might take several minutes.
11- 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.
12- If synthesis succeeds, you will be prompted with the next step. Select "Run Implementation" and wait a few more minutes (tipically ~3-10 minutes).
13- If implementation succeeds select "Generate Bitstream" in the following window. This will generate the configuration binary to step up the FPGA according to EILID hardware and software.
14- 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.
15- Right-click your FPGA and select "Program Device" to program the FPGA.
To simulate EILID using VIVADO sim-tools, continue following the instructions on [Running EILID on Vivado Simulation Tools].
After completing the steps 1-11 in [Creating a Vivado Project for EILID]:
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 sample application does the following steps:
- The application aims to read temperature sensor and humidity sensor periodically.
- At first, at the beginning of main(), NS_EILID_store_ind() is called to store all function entry points in the shadow stack.
- During its execution, the rest steps are repeated to guarantee control-flow integrity in certain conditions.
- Before a function call (e.g. initSensor(), readTemperature()), NS_EILID_store_ra() is invoked to store its return address.
- Steps A and C are executed.
- Before a function return (i.e. 'ret' instruction), NS_EILID_check_ra() is invoked to validate if the address it is returning to is the same as the one stored in the shadow stack.
- Steps B and C is executed.
- If an interrupt is triggered, at the beginning of the interrupt service routine (ISR), NS_EILID_store_rfi() is called to store the interrupt context (Status register (R2) and return address).
- Steps A and C are executed.
- Before a ISR return (i.e. 'reti' instruction), NS_EILID_check_rfi() is invoked to validate if the interrupt context it currently has is the same as the one stored in shadow stack.
- Steps B and C are executed.
- Before an indirect call, NS_EILID_check_ind() is invoked to validate if the address it is jumping to is the same as the one in the shadow stack.
- Steps B and C are executed.
Special steps to switch SW:
- A: (Normal SW->Trusted SW): Store values in Shadow stack It goes to (0xA000), an entry of secure ROM, to execute the corresponding authorized function (S_EILID_ functions), to store given values. Also, stack pointer (r1) is switched to point to secure stack (0x1000).
- B: (Normal SW->Trusted SW): Check values with the ones stored in Shadow stack It goes to (0xA000), an entry of secure ROM, to execute the corresponding authorized function (S_EILID_ functions), to load the stored addresses. Also, stack pointer (r1) is switched to point to secure stack (0x1000). If the loaded address is identical to its returning address, it continues; otherwise, it branchs to the reset handler.
- C: (Trusted SW->Normal SW) It returns to the place where it left for resuming normal operation (with main stack, ~0x6200).
- (Normal SW->Trusted SW) Store function entry point at the beginnning of main(). NS_EILID_store_ind() is called at (0xE042) and switched to CASU_init() at (0xA000) after 5 instuctions. Stack pointer (r1) is changed from main stack (0x61FA) to secure stack (0x1000). Function entry point (0xE096, the address of digitalRead() in this case) is loaded in r6 as below:
- (Trusted SW->Normal SW) Return to the normal operation. Stack pointer (r1) is changed from secure stack (0x1000) to normal stack (0x61FA) as below:
- (Normal SW->Trusted SW) Store return address before function call (initSensor() in this case). NS_EILID_store_ra() is called at (0xE1EC) and switched to CASU_init() at (0xA000) after 5 instuctions. Stack pointer (r1) is changed from main stack (0x61E8) to secure stack (0x1000). Return address (0xE1F4, 0xE1EC + 8 in this case) is loaded in r6 as below:
- (Trusted SW->Normal SW) Return to the normal operation. Stack pointer (r1) is changed from secure stack (0x1000) to normal stack (0x61E8) as below:
- (Normal SW->Trusted SW) Check return address before function return (initSensor() in this case). NS_EILID_check_ra() is called at (0xE172) and switched to CASU_init() at (0xA000) after 5 instuctions. Stack pointer (r1) is changed from main stack (0x61E6) to secure stack (0x1000). Run-time return address loaded from main stack (0xE1F4 in this case) is loaded in r6. It will be compared with the one stored in shadow stack (0xE1F4) as below:
- (Trusted SW->Normal SW) Return to the normal operation. Stack pointer (r1) is changed from secure stack (0x1000) to normal stack (0x61E6) as below:
Recall that EILID does not require any further hardware modification on CASU hardware. In other words, hardware verification of EILID is the same as the one of CASU. To verify EILID (CASU) hardware, firstly, we need to install the verification tools:
cd scripts
make install
To check HW-Mod against EILID properties using NuSMV run:
make verify
EILID properties (along with VRASED ones) are in:
verification_specs/ltl_specs.smv