Trustworthy and Distributed Automated Reasoning

Guaranteeing runtime integrity of embedded system software is an open problem. Trade-offs between security and other priorities (e.g., cost and/or performance) are inherent, and resolving them is both challenging and important. Proliferation of runtime attacks that introduce malicious code (e.g., by injection) into embedded devices motivates research into mitigation techniques. One popular approach is Remote Attestation (RA), whereby a trusted entity (verifier) periodically checks the current software state of an untrusted remote device (prover). RA yields a timely authenticated snapshot of prover's state that verifier uses to decide whether an attack/compromise occurred.

One major issue is that RA represents pure overhead and can consume non-negligible time and other resources on prover, which is problematic for a real-time or safety-critical device. Consequently. there is a need to minimize RA time complexity. To address this problem, we show how to construct a low-overhead RA technique that consumes very little bandwidth and minimal amount of cryptographic overhead.
Another issue is that current RA approaches require verifier to explicitly initiate RA, based on some unclear criteria. Thus,, verifier only learns about prover's compromise 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 an inexpensive hardware/software co-design enforcing: (i) runtime software immutability, thus precluding any illegal software modification, and (ii) authenticated updates as the sole means of modifying software. In it, a successful RA instance serves as a proof of successful update, and continuous subsequent software integrity is implicit, due to the runtime immutability guarantee. This obviates the need for RA between software updates and yields unobtrusive integrity assurance.