【終了】第4回ステアラボソフトウェア技術セミナー 池渕未来 様「Certifying Derivation of State Machines from Coroutines」 The 4th STAIR Lab ST Seminar: Dr. Mirai Ikebuchi, "Certifying Derivation of State Machines from Coroutines"

We have been regularly organizing STAIR Lab AI seminars, which mainly focus on artificial intelligence topics including machine learning, natural language processing, and so on. In addition to them, we decided to hold STAIR Lab ST seminars online, which focus on research topics in software technology.

千葉工業大学 人工知能・ソフトウェア技術研究センター (ステアラボ) では、従来機械学習や自然言語処理等の人工知能に関するセミナー (ステアラボ人工知能セミナー) を開催して参りましたが、この度、ソフトウェア技術研究に関するセミナーもオンライン形式で開催することに致しました。

Everyone can participate for free. Theoretically, there is no limit on the number of participants because they are held online.
We are looking forward to your participation.

どなたでも無料でご参加いただけます。オンライン形式のため特に定員数は設けておりませんので皆様奮ってご参加ください。

【日時】
2022 年 4月 21 日 (木) 15:00 – 16:00

Date:
Apr. 21, 2022 (Thu.) 15:00 – 16:00

【講演形態】
オンライン

Venue:
Online

【講演者】
国立情報学研究所 池渕 未来 様
https://mir-ikbch.github.io/

Speaker:
Dr. Mirai Ikebuchi, National Institute of Informatics
https://mir-ikbch.github.io/

【講演タイトル】
Certifying Derivation of State Machines from Coroutines

Title:
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.

Abstract:
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.

The details are written in Japanese and the talk will be given in Japanese.