Formal Proofs of Realistic Programs using Separation Logic

点击翻译按钮获取中文摘要

With the dissemination of embedded systems, it has become important to provide strong security guarantees for low-level programs. According to international standards, the most reliable evaluation assurance method is formal verification. Unfortunately, given the current state of the art, it is still difficult to perform formal verification of large programs. Yet, low-level programs are characterized by detailed memory manipulations, for which the formalism of Separation Logic has been proposed by researchers. In this project, we have developed an environment for formal verification based on Separation Logic, whose usefulness is demonstrated by realistic case studies(SmartMIPS implementations of a pseudorandom number generator and signed multi-precision arithmetic, including the binary extended GCD algorithm, as used in the implementation of cryptographic schemes).