We solve this problem in two steps. First, we introduce a contract layer between the (CPU) hardware and the software that allows the specification of microarchitectural side-effects on masked software in an intuitive language. Second, we present a method for proving the correspondence between contracts and CPU netlists to ensure the completeness of the specified leakage models. Then, any further security proofs only need to happen between software and contract, which brings benefits such as reduced verification runtime, improved user experience, and the possibility of working with vendor-supplied contracts of CPUs whose design is not available on netlist-level due to IP restrictions. We apply our approach to the popular RISC-V IBEX core, provide a corresponding formally verified contract, and describe how this contract could be used to verify masked software implementations.
Category / Keywords: foundations / Power Side-Channel, Leakage Model, Verification, Contract, Domain-Specific Language, Masking, Probing Security Date: received 9 May 2022 Contact author: vedad hadzic at iaik tugraz at Available format(s): PDF | BibTeX Citation Version: 20220510:082439 (All versions of this report) Short URL: ia.cr/2022/565