Verification of Hardware and Software with Fuzzing and Proofs
summary
A verification methodology proves end-to-end security of an authenticated firmware loader on a small SoC model and checks typical attacks like TOCTOU by encoding hyper properties and verifying pairs of traces, with successful proofs completing in seconds on the prototype model. A testing framework HyperFuzzing specifies hardware security as hyper-properties and generates counterexample trace pairs via fuzzing. An SMT prototype Sādhak implements a closed-box function theory, purifies queries, delegates executable components to fuzzing, and the combined SMT+fuzzing pipeline finds satisfiable bugs faster than either technique alone.
AI-written summary · about
chapters (6)
- 0:00Verification challenges
- 2:52Firmware loader verification
- 10:29Fuzzing for scalable testing
- 15:24Hybrid methods
- 17:54Future research
- 18:36Q&A
related talks
01h 08mProviding evidence for the security properties of hardware/software codesigns
34mFormally verified hardening of C programs against hardware fault injection
01h 15mMake your programs more reliable with Fuzzing
01h 04mSoftware Verification meets Real-World Cryptography
20mFSLH: Flexible Mechanized Speculative Load Hardening
32mFuzzing Zephyr Apps - Struggles of Dynamic Analysis on Embedded Applications
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
39mKeynote: Towards High-Assurance Cryptographic Software