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

Question

seL4是一个经过正式验证的操作系统。在这个pdf中，它说“没有算术或其他异常”。如何验证这一点？实现是不是强制每个有效的输入？

Answer 1

这绝对不是蛮力！

已经尝试了许多不同的技术来建立算法安全，并取得了不同程度的成功。如今，大多数计算机算术都是完全形式化的，既有形式化的，如Isabelle/HOL，Coq，ACL2，也有许多其他定理证明器；也有更自动化的技术，如SMT求解。在这些系统中，您将获得系统的模型(手动编写或从实际源代码中自动提取)，然后证明在执行过程中没有遇到溢出/下溢的路径。当然，这说起来容易做起来难；但随着时间的推移，工具支持一直在稳步改善。

要了解如何或多或少地自动检测算术溢出/下溢，值得一看的一篇很好的论文是Nikolaj在SMT领域内的工作：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf中包含的参考文献也可以作为一个很好的起点来查看沿着这些路线进行的其他研究。