Formal Proofs of Realistic Programs using Separation Logic

随着嵌入式系统的普及，为底层程序提供强有力的安全保障变得越来越重要。根据国际标准，最可靠的评价保证方法是形式验证。不幸的是，考虑到目前的技术状态，对大型程序进行正式验证仍然很困难。然而，低级程序的特点是详细的内存操作，为此，研究者提出了分离逻辑的形式主义。在这个项目中，我们开发了一个基于分离逻辑的形式化验证环境，其实用性通过实际案例研究（在加密方案实现中使用的伪随机数生成器和签名多精度算法的SmartMIPS实现，包括二进制扩展GCD算法）得到了证明。

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).