A Deductive System for Contract Satisfaction Proofs

Arthur Correnson, Haoyi Zeng, Jana Hofmann

Hardware-software contracts are abstract specifications of a CPU's leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without…