如何正式验证 "没有算术或其他异常"？

Posted 2023-01-05

seL4是一个经过正式验证的操作系统。在这个 pdf 上面写着 "无算术或其他例外情况"。如何验证呢？是否实现了对每一个有效的输入都进行了粗暴的强制？

答案

这绝对不是粗暴强迫!

人们尝试了很多不同的技术来建立算术安全，但都取得了不同程度的成功。现在大多数计算机算术都已经完全形式化了，既包括IsabelleHOL、Coq、ACL2等形式化的定理证明器；也包括SMT求解等更自动化的技术。在这些系统中，你得到一个系统的模型（可以是手工写的，也可以是从实际的源代码中自动提取的），然后你要证明你的执行中没有遇到过流的路径。当然，这说起来容易，做起来难；但随着时间的推移，工具的支持也在稳步提高。

要想了解如何或多或少地自动检测算术溢出underflow，可以看看Nikolaj在SMT领域内的工作，这是一篇很棒的论文。https:/www.microsoft.comen-usresearchwp-contentuploads201602z3prefix.pdf 这里面的参考资料也可以作为一个很好的起点，按照这个思路去看其他的研究。