Isolation Without Taxation: Near Zero Cost Transitions for WebAssembly and SFI

Cryptographic Capability Computing

Network-on-Chip Firewall: Countering Defective and Malicious System-on-Chip Hardware

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.

Reliable telemetry in white spaces using remote attestation

Enforcing Executing-Implies-Verified with the Integrity-Aware Processor

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.

Diagnostic Powertracing for Sensor Node Failure Analysis

Sh@re: Negotiated audit in social networks

Cumulative Attestation Kernels for Embedded Systems

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.

Collaborative Recommender Systems for Building Automation

An Integrated Architecture for Demand Response Communications and Control (best paper award)

Price-responsive electrical demand-response system, e.g. for laptops and air conditioners, with multiple loci of control.