VISPR: A Verified Instruction Secure Processor
VISPR: A Verified Instruction Secure Processor
Project Summary
Processor security is a foundational challenge: an adversary who compromises instruction fetch or decode can undermine any software-layer defense. The VISPR project designed and prototyped a formally verified secure processor that provides hardware-enforced guarantees about instruction integrity and execution correctness.
Research contributions include:
- Formal verification of processor microarchitecture: Applying formal methods to prove security properties of the instruction pipeline
- Hardware isolation primitives: Mechanisms that enforce separation between privileged and unprivileged execution contexts at the microarchitecture level
- Industry collaboration: Working with Clarity Cyber, LLC to develop practical security enhancements applicable to real embedded systems
Funding
This project was supported by the Maryland Industrial Partnerships (MIPS) program. Industry subaward recipient: Clarity Cyber, LLC.