このエントリーをはてなブックマークに追加

Apr

21

第4回ステアラボソフトウェア技術セミナー

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

Organizing : 千葉工業大学 人工知能・ソフトウェア技術研究センター

Hashtag :#stairlab
Registration info

参加枠

Free

Attendees
37

参加者への情報
(参加者と発表者のみに公開されます)

Description

国立情報学研究所 池渕未来 様: 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.

Media View all Media

If you add event media, up to 3 items will be shown here.

Feed

toshi_m

toshi_m published 第4回ステアラボソフトウェア技術セミナー.

04/06/2022 16:52

第4回ステアラボソフトウェア技術セミナー を公開しました!

Group

Ended

2022/04/21(Thu)

15:00
16:00

Registration Period
2022/04/06(Wed) 16:52 〜
2022/04/21(Thu) 16:00

Location

オンライン

オンライン

オンライン

Organizer

Attendees(37)

Sato, Ryosuke

Sato, Ryosuke

第4回ステアラボソフトウェア技術セミナー に参加を申し込みました!

Daisuke_Kimura

Daisuke_Kimura

I joined 第4回ステアラボソフトウェア技術セミナー!

hide-kawabata

hide-kawabata

第4回ステアラボソフトウェア技術セミナー に参加を申し込みました!

tsakama

tsakama

第4回ステアラボソフトウェア技術セミナー に参加を申し込みました!

kk20150824

kk20150824

第4回ステアラボソフトウェア技術セミナー に参加を申し込みました!

KanSAKAMOTO

KanSAKAMOTO

第4回ステアラボソフトウェア技術セミナー に参加を申し込みました!

yukiyama999999999999913

yukiyama999999999999913

第4回ステアラボソフトウェア技術セミナー に参加を申し込みました!

klnW

klnW

第4回ステアラボソフトウェア技術セミナーに参加を申し込みました!

Tamaki Okui

Tamaki Okui

I joined 第4回ステアラボソフトウェア技術セミナー!

Makinori Ikegami

Makinori Ikegami

第4回ステアラボソフトウェア技術セミナー に参加を申し込みました!

Attendees (37)

Canceled (1)