1

We developed a Network-on-Chip (NoC) firewall in Bluespec SystemVerilog configured by a dedicated core, and we demonstrated how it can enforce isolation between two instances of Linux on separate cores. We developed a shallow embedding of a subset of Bluespec into Maude, since both languages are based on term rewriting systems, and we used a Maude model of the NoC firewall to precisely identify a subtle vulnerability.

Extended a processor core written in VHDL with hardware support for detecting attempts to execute unverified code. Developed an integrity kernel and network server to enforce code whitelisting using processor extensions. Evaluated using an FPGA.

Developed kernel for flash MCUs that continuously monitors firmware controlling each microcontroller and reports to remote parties, using Elliptic Curve Cryptography to authenticate the audit log. Kernel provides fault-tolerance using mechanisms that were formally verified using the Maude model checker.