Automatic and Incremental Repair for Speculative Information Leaks.

Summary

We present CURESPEC, the first model-checking based framework for automatic repair of programs with respect to information leaks in the presence of side-channels and speculative execution. CURESPEC is based on formal models of attacker capabilities, including observable side channels, inspired by the SPECTRE-PHT attacks. For a given attacker model, CURESPEC is able to either prove that the program is secure, or detect potential side-channel vulnerabilities and automatically insert mitigations such that the resulting code is provably secure. Moreover, CURESPEC can provide a certificate for the security of the program that can be independently checked. We have implemented CURESPEC in the SeaHorn framework and show that it can effectively repair security-critical code, for example the AES encryption from the OpenSSL library.