Place: Conference Room no. 2, Auditorium, Central 1, Tsukuba Central. Access information.
場所：つくば中央, 第1事業所, 共用講堂, 中会議室. 交通アクセス
Venue information 会場情報
概要：
Formal Network Packet Processing with Minimal Fuss: Invertible Syntax Descriptions at Work
An error in an Internet protocol or its implementation is rarely benign: at best, it leads to malfunctions, at worst, to security holes. These errors are all the more likely that the official documentation for Internet protocols (the RFCs) is written in natural language. To prevent ambiguities and pave the way to formal verification of Internet protocols and their implementations, we advocate formalization of RFCs in a proof-assistant. As a first step towards this goal, we propose in this paper to use invertible syntax descriptions to formalize network packet processing. Invertible syntax descriptions consist in a library of combinators that can be used interchangeably as parsers or pretty-printers: network packet processing specified this way is not only unambiguous, it can also be turned into a trustful reference implementation, all the more trustful that there is no risk for inconsistencies between the parser and the pretty-printer. Concretely, we formalize invertible syntax descriptions in the Coq proof-assistant and extend them to deal with data-dependent constraints, an essential feature when it comes to parsing network packets. The usefulness of our formalization is demonstrated with an application to TLS, the protocol on which e-commerce relies.
Freek Wiedijk [1, 2007] [1bis, 2007] は、定理証明器の評価と比較のための ベンチマークとして、「√2 は無理数であること」の証明を集めた。 Thierry Coquand [2, 2007] は Wiedijk の要求に応え、 Agda1/Alfa での証明を書いた。しかし、現在 Agda1/Alfa は 開発が停止し、用いることができない。Agda1/Alfa の後継として 開発されている Agda2 [3] では文法の違いにより Coquand の 証明譜を検査することができない。私の知るかぎり、Agda2 による 「√2 は無理数」の証明は無いので、それを書いた [4] 。 Agda1/Alfa を含む他の定理証明器と Agda2 の相違点など、 Coquand の証明譜を翻訳したことで得られた知見を紹介する。