Formal verification of low-level software has become a trend in the formal methods community. This is justified by the fact that our lives rely on this software: brake systems of cars, flying controls of airplanes, vital medical devices, or security probes of power plants. Beyond the stakes, the difficulty also motivates the community. Indeed this software verification presents a challenge: they are complex, often written in different languages and they implement subtle control-flow.

In this thesis, we study the formal verification of a particular case of lowlevel software: operating system kernels. As a test-bed we have chosen Topsy, an embedded operating system for network devices. This kind of software has the particularity to run user applications, to provide them services and to make the interface with the underlying hardware. Our main interest is about the interaction between the kernel and its user applications. Our study starts from an abstract view of the system, implemented as a model of the hardware, the kernel and its applications in the SPIN model checker. We use this abstraction to verify properties about the message passing services and the protection of the kernel memory. For this latter property we identify some parts of the code that are sensible, such as the memory allocation and the context switching. The next step is to verify the source code implementing these facilities. For this purpose we model both a C-like language and the MIPS assembly, inside the Coq proof assistant, as well as a well-known extension of Hoare-logic: the separation logic. Using these implementations we verify the memory allocator and application context switching code of Topsy. Through this experiences, we come to investigate the automation of code verification. We also implement an original and certified verification function for separation logic triples inside of Coq. This function can be extracted as a stand-alone and certified verifier. We apply this verifier on the verification of a library for lists, which is a must have for operating system kernels, and to the thread creation function of Topsy.

本論文は、オペレーティングシステムカーネルにおけるメモリ領域の保護に関する性質を形式的に検証するための新しい技術に関して述べている。近年、組込みシステムのソフトウェア等、ハードウェアに近い低レベルのソフトウェアの形式的検証の研究が活発である。しかし、低レベルソフトウェアは複雑であり、しばしば複数のプログラミング言語で記述され、しかも難解な制御フローを実装しているため、その検証は極めて困難である。

本研究では、そのような低レベルソフトウェアにおける最も基本的な性質であるメモリ領域の保護に関して、分離論理と呼ばれる枠組みのもとで、正当性が保証されしかも効率のよい検証系を構築し、C言語および機械語で書かれたプログラムの検証に成功した。しかも、本研究は、ネットワークデバイスのための組み込みオペレーティングシステムであるTbpsyを形式的検証の具体的な対象としている。

本論文の第1章では本研究の背景とアプローチについて概説されている。本論文の以下の部分は第一部と第二部から成り立っている。

第一部では、まず第2章において、Hoare論理の拡張である分理論理、Coq証明支援系、Tbpsyに関する背景知識が説明された後、第3章において、Coq上で分離論理の公理化が行われたうえで、Coqのタクティクを用いて、リスト操作を行うC言語風のプログラムの検証が行われている。第4章においては、有限長の整数理論の上で、コンテキストスイッチングを行うMIPS風の機械語のプログラムの検証が行われている。

第二部では検証ツールについて述べられている。第5章において、形式的検証を効率化するために、Coq上に効率のよい検証系が構築され、その正当性が形式的に検証されたうえで、形式的証明から取り出されたCamlのプログラムによって実際に検証が効率よく行えることが示されている。第6章では、C言語風のプログラムから機械語のプログラムへの翻訳系の正当性が形式的に検証され、検証済みのCプログラムから検証済みの機械語プログラムが得られることが示されている。

第7章では本論文の貢献についてまとめられている。

以上で述べたように、本研究は低レベルソフトウェアの形式的検証の技術を大きく進展させており、本論文は博士(情報理工学)の学位請求論文として合格と認められる。