Postscript: あとがき


Congratulations: We've made it to the end!

ふりかえり


ここまで様々なことを学んできました。 「論理の基礎」から始まった軌跡を振り返ってみましょう。
  • 関数プログラミング
    • 「宣言的」プログラミング（変更可能な配列やポインタなどによるループではなく、不変データ構造上の再帰）
    • 高階関数
    • 多相性

  • 論理、ソフトウェア工学の数学的基盤: 
                    論理                        微積分
        --------------------   ~   ---------------------------- 
            ソフトウェア工学               機械/土木工学
    • 帰納的に定義された集合と関係
    • 帰納的証明
    • 証明オブジェクト

  • Coq、産業用途に耐え得る証明支援器
    • 関数型のコア言語
    • 基礎となるタクティック
    • 自動化

  • プログラミング言語の基礎
    • 以下を精密に定めるための記法と定義法
      • 抽象構文
      • 操作的意味
        • 大ステップ形式
        • 小ステップ形式
      • 型システム
    • プログラム同値性
    • ホーア論理
    • 型システムの基本的メタ理論
      • 進行と保存
    • サブタイプ理論

Looking Around

Large-scale applications of these core topics can be found everywhere, both in ongoing research projects and in real-world software systems. Here are a few recent examples involving formal, machine-checked verification of real-world software and hardware systems, to give a sense of what is being done today...

CompCert

CompCert is a fully verified optimizing compiler for almost all of the ISO C90 / ANSI C language, generating code for x86, ARM, and PowerPC processors. The whole of CompCert is is written in Gallina and extracted to an efficient OCaml program using Coq's extraction facilities.
"The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs."
In 2011, CompCert was included in a landmark study on fuzz-testing a large number of real-world C compilers using the CSmith tool. The CSmith authors wrote:
  • The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.
http://compcert.inria.fr

seL4

seL4 is a fully verified microkernel, considered to be the world's first OS kernel with an end-to-end proof of implementation correctness and security enforcement. It is implemented in C and ARM assembly and specified and verified using Isabelle. The code is available as open source.
"seL4 has been comprehensively formally verified: a rigorous process to prove mathematically that its executable code, as it runs on hardware, correctly implements the behaviour allowed by the specification, and no others. Furthermore, we have proved that the specification has the desired safety and security properties (integrity and confidentiality)... The verification was achieved at a cost that is significantly less than that of traditional high-assurance development approaches, while giving guarantees traditional approaches cannot provide."
https://sel4.systems.

CertiKOS

CertiKOS is a clean-slate, fully verified hypervisor, written in CompCert C and verified in Coq.
"The CertiKOS project aims to develop a novel and practical programming infrastructure for constructing large-scale certified system software. By combining recent advances in programming languages, operating systems, and formal methods, we hope to attack the following research questions: (1) what OS kernel structure can offer the best support for extensibility, security, and resilience? (2) which semantic models and program logics can best capture these abstractions? (3) what are the right programming languages and environments for developing such certified kernels? and (4) how to build automation facilities to make certified software development really scale?"
http://flint.cs.yale.edu/certikos/

Ironclad

Ironclad Apps is a collection of fully verified web applications, including a "notary" for securely signing statements, a password hasher, a multi-user trusted counter, and a differentially-private database.
The system is coded in the verification-oriented programming language Dafny and verified using Boogie, a verification tool based on Hoare logic.
"An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app’s behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times. We provide these guarantees via complete, low-level software verification. We then use cryptography and secure hardware to enable secure channels from the verified software to remote users."
https://github.com/Microsoft/Ironclad/tree/master/ironclad-apps

Verdi

Verdi is a framework for implementing and formally verifying distributed systems.
"Verdi supports several different fault models ranging from idealistic to realistic. Verdi's verified system transformers (VSTs) encapsulate common fault tolerance techniques. Developers can verify an application in an idealized fault model, and then apply a VST to obtain an application that is guaranteed to have analogous properties in a more adversarial environment. Verdi is developed using the Coq proof assistant, and systems are extracted to OCaml for execution. Verdi systems, including a fault-tolerant key-value store, achieve comparable performance to unverified counterparts."
http://verdi.uwplse.org

DeepSpec

The Science of Deep Specification is an NSF "Expedition" project (running from 2016 to 2020) that focuses on the specification and verification of full functional correctness of both software and hardware. It also sponsors workshops and summer schools.
  • Website: http://deepspec.org/
  • Overview presentations:
    • http://deepspec.org/about/
    • https://www.youtube.com/watch?v=IPNdsnRWBkk

REMS

REMS is a european project on Rigorous Engineering of Mainstream Systems. It has produced detailed formal specifications of a wide range of critical real-world interfaces, protocols, and APIs, including the C language, the ELF linker format, the ARM, Power, MIPS, CHERI, and RISC-V instruction sets, the weak memory models of ARM and Power processors, and POSIX filesystems.
"The project is focussed on lightweight rigorous methods: precise specification (post hoc and during design) and testing against specifications, with full verification only in some cases. The project emphasises building useful (and reusable) semantics and tools. We are building accurate full-scale mathematical models of some of the key computational abstractions (processor architectures, programming languages, concurrent OS interfaces, and network protocols), studying how this can be done, and investigating how such models can be used for new verification research and in new systems and programming language research. Supporting all this, we are also working on new specification tools and their foundations."
http://www.cl.cam.ac.uk/~pes20/rems/

Others

There's much more. Other projects worth checking out include:
  • Vellvm (formal specification and verification of LLVM optimization passes)
  • Zach Tatlock's formally certified browser
  • Tobias Nipkow's formalization of most of Java
  • The CakeML verified ML compiler
  • Greg Morrisett's formal specification of the x86 instruction set and the RockSalt Software Fault Isolation tool (a better, faster, more secure version of Google's Native Client)
  • Ur/Web, a programming language for verified web applications embedded in Coq
  • the Princeton Verified Software Toolchain

これからの指針


先に進む資料としてよいものをいくつか...
  • この本のオプションの章。 目次と依存関係のページを眺めてみてください。
  • ホーア論理とプログラム検証について:
    • The Formal Semantics of Programming Languages: An Introduction, by Glynn Winskel Winskel 1993 （Bib.v内）
    • 実践的な形式検証ツール、例えばMicrosoftのBoogie system、Java Extended Static Checking、など
  • プログラミング言語の基礎について:
    • Concrete Semantics with Isabelle/HOL, by Tobias Nipkow and Gerwin Klein Nipkow 2014 （Bib.v内）
    • Types and Programming Languages, by Benjamin C. Pierce Pierce 2002 （Bib.v内） （和訳：型システム入門 -プログラミング言語と型の理論-）
    • Practical Foundations for Programming Languages, by Robert Harper Harper 2016 （Bib.v内）
    • Foundations for Programming Languages, by John C. Mitchell Mitchell 1996 （Bib.v内）
  • Iron Lambda (http://iron.ouroborus.net/) は、段階的に複雑さが変わる複数の関数型言語のCoqによる定式化です。 ソフトウェアの基礎と、最近の研究論文で起こっていることのギャップを埋めてくれます。 定式化の中では、STLCや多相ラムダ計算（System F）の複数の亜種について、少なくとも進行性定理や型保存定理が示されています。
  • 最後に、プログラミング言語と形式検証について最先端を行く学会:
    • Principles of Programming Langauges (POPL)
    • Programming Language Design and Implementation (PLDI)
    • International Conference on Functional Programming (ICFP)
    • Computer Aided Verification (CAV)
    • Interactive Theorem Proving (ITP)
    • Certified Programs and Proofs (CPP)
    • SPLASH/OOPSLA
    • Principles in Practice workshop (PiP)
    • CoqPL workshop