聪明人的笨功夫 -- MesaTEE安全形式化验证实践

2019-08-08 16:21:5914643人阅读

本文诠释了形式化验证的原理，分享了MesaTEE对实际工程项目进行形式化验证的经验，特别是对TPM核心软件栈和MesaPy C backend的验证。实践证明，通过形式化验证来保证代码安全虽然成本昂贵，但通过精心设计还是切实可行的。除此之外，形式化验证还是能够更透彻地发现程序安全缺陷，并且保障程序在给定约束下是安全的。