FM

Reference:

形式化方法是一种用把复杂系统描述为数学模型的方法。 通过把复杂的系统定义为逻辑严密的数学模型， 可以利用数学的方法验证系统的一些属性， 这类方法往往比基于经验的测试更全面彻底。

虽然严密的数学方法能够有效的提高系统的可靠性，节省设计时间，增强可理解性，但学习或培训此类方法的周期比较长；而传统的工程教学并不会教授如何用形式化的数学方法描述一个计算系统。并且，各类形式化方法中的模型都会为了提高可证明性而增加各类限制规则。因此，在形式化方法的描述能力和严密程度上，必须做出取舍。

形式化方法使用数学证明辅以系统测试，来保证被测试系统的行为准确性。随着系统变得越来越复杂，安全变得更为重要，形式化方法对系统设计提供了更高的安全保障。

迪杰斯特拉（Dijkstra）等人已经展示过，通过测试的方法只能看出系统在什么样的情况下不会fail，但无法了解到对于测试用例之外的任何情况。相反的，如果一个数学定理被证明为正确，那么它将一直是正确的。

有一点很重要，就是形式化验证并不能完全取代测试[Bowen95]。

形式化方法的三个步骤：

  1. 形式化定义(formal specification)：在定义阶段，工程师使用一个模型语言(modeling languages)描述一个系统。这个过程类似于一个把word文档描述的问题转换为一个用数学代数语言描述的问题。
  2. 验证：
  3. 实现：一旦一个模型通过了定义和验证阶段，下一步就是把模型的定义转换成代码。

形式化方法的作用一直是广受怀疑的。自1960年代，形式化方法的研究便已经开始，但是工程师们接受这类方法的过程是相当缓慢的。这又多方面的原因，但是多数的原因是对形式化方法的错误应用。大多数的形式化系统的描述能力是相当强大的，多数建模语言在设计时都会把能够描述一切作为重要标准。

工业应用

The growth in complexity of designs increases the importance of formal verification techniques in the hardware industry.[6][7] At present, formal verification is used by most or all leading hardware companies,[8] but its use in the software industry is still languishing.[citation needed] This could be attributed to the greater need in the hardware industry, where errors have greater commercial significance.[citation needed] Because of the potential subtle interactions between components, it is increasingly difficult to exercise a realistic set of possibilities by simulation. Important aspects of hardware design are amenable to automated proof methods, making formal verification easier to introduce and more productive.[9]

  • Basic Concepts

    • References: Terms Orderings Model Checking Temporal Logic https://plato.stanford.edu/entries/logic-temporal/ In order to ensure correct behavior of a reactive program, in which computations are non-terminating (e.g. an operating system), it is necessary to formally specify and verify the acceptable infinite executions of that program. In addition, to ensure correctness of a concurrent program, where two or more processors are working in parallel, it is necessary to formally specify and verify their interaction and synchronization.

  • Constructive Logic

    • Reference 1 CMU Undergraduate Class ↩

  • Abstract Algebra

    • Reference 1 The Group Groups Reference 1 reference ↩ reference ↩

  • Galois

    • Reference 1 -- > Listen Galois pronunciation from 4:30 Galois Connection ↩

  • Abs Int

    • PPA version Reference 1 The theory of Abstract Interpretation is a general methodology for calculating analyses rather than just specifying them and then rely on a posteriori validation. Collecting Semantics records the set of traces $tr$ that can reach a given program point: $tr \in Trace = (Var \times Lab)^*$ e.g: $((x, ?), (y, ?), (z, ?), (y, 1), (z, 2), (z, 4), (y, 5), (z, 4), (y, 5), (y, 6))$

  • Papers

    • Reference 1 CSpec Reference 1 201901 note. Verifying concurrent software using movers in CSPEC. OSDI, 2018. ↩ 2019 Arm Os Reference 1 Scalable Translation Validation of Unverified Legacy OS Code. FMCAD, 2019. ↩ Intscope Reference 1 Decompiler: Bestar, IDA Pro as front-end. translates x86 assembl into PANDA IR (freshly designed). Symbolic execution engine: leverage framework of GiNac[^c8]. Path Validator and Integer Overflow Checker: STP, a decision procedure for bit-vectors and arrays.

  • Temporal Logic

    • Reference 1 CTL References: Lecture 7, Computation Tree Logics Path Quantifier $A$: for every path. $E$: there exists a path. Linear-time operators $\boldsymbol{X}_p$: $p$ holds next time. $\boldsymbol{F}_p$: $p$ holds sometime in the future. $\boldsymbol{G}_p$: $p$ holds globally in the future. $p\boldsymbol{U}q$: $p$ holds until $q$ holds. Path Formulas and State Formulas More reference ↩

  • Model Checking

    • References: Model Checking @CMU Model Checking Code @CMU Specification and Verification Center @CMU wiki: Model Checking, contains a list of model checking tools. Model Checking简述

  • Hott

    • Reference1 “Homotopy Type Theory: Univalent Foundations of Mathematics”. ↩

  • Separation Logic

    • References: Separation Logic, Peter O’Hearn Separation logic, first developed by O’Hearn and Reynolds, is an extension of Hoare’s logic which addresses reasoning about program that access and mutate data structures. It includes a “frame rule” which enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specification and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.

Created Jul 30, 2019 // Last Updated Dec 6, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?