国立情報学研究所 池渕未来 様: Certifying Derivation of State Machines from Coroutines

千葉工業大学 人工知能・ソフトウェア技術研究センター (ステアラボ) では、従来機械学習や自然言語処理等の人工知能に関するセミナー (ステアラボ人工知能セミナー) を開催して参りましたが、この度、ソフトウェア技術に関連する最先端の研究について第一線の研究者をお招きしてご講演頂く「ステアラボソフトウェア技術セミナー」をオンライン形式で開催することに致しました。

今回は国立情報学研究所の池渕未来様に「Certifying Derivation of State Machines from Coroutines」というタイトルでご講演いただきます。

どなたでも無料でご参加いただけます。 参加申し込みをして頂くと具体的なアクセス情報が表示されます。オンライン形式のため特に定員数は設けておりませんので皆様奮ってご参加ください。

※ ただし、あまりに多数の申し込みを頂いた場合は参加登録を打ち切る等の対応をさせて頂く可能性もございますのでその際は何卒ご容赦下さい。

日時

2022年4月21日 (木) 15:00-16:00

講演形態

• オンライン: Microsoft Teams を使用します。
  • (不具合等により万が一 Microsoft Teams が使用できない場合は、バックアップとして Cisco Webex Meetings を使用します。)
• アクセス方法は参加登録をして頂いた方にのみ公開されます。

講演者

国立情報学研究所 池渕 未来 様

講演タイトル

Certifying Derivation of State Machines from Coroutines

講演概要

One of the biggest implementation challenges in security-critical network protocols is nested state machines. In practice today, state machines are either implemented manually at a low level, risking bugs easily missed in audits; or are written using higher-level abstractions like threads, depending on runtime systems that may sacrifice performance or compatibility with the ABIs of important platforms (e.g., resource-constrained IoT systems). We present a compiler-based technique allowing the best of both worlds, coding protocols in a natural high-level form, using freer monads to represent nested coroutines, which are then compiled automatically to lower-level code with explicit state. In fact, our compiler is implemented as a tactic in the Coq proof assistant, structuring compilation as search for an equivalence proof for source and target programs. As such, it is straightforwardly (and soundly) extensible with new hints, for instance regarding new data structures that may be used for efficient lookup of coroutines. As a case study, we implemented a core of TLS sufficient for use with popular Web browsers, and our experiments show that the extracted Haskell code achieves reasonable performance.