EuroSys 2024 でポスター発表

参照モニタの形式検証に関する研究

EuroSys 2024 でのポスター発表の様子

品川研究室の中島諒くん(システム情報学専攻修士課程2年)が、2024年4月にギリシャで開催された国際会議 The European Conference on Computer Systems (EuroSys) 2024 でポスター発表をしました。

本研究では、サンドボックスやTEEなどの隔離実行環境を形式検証によりセキュリティ強化することを目的として、効果的かつ現実的な形式検証の適用を可能にするために、アクセス制御を実施する中心的なコンポーネントである参照モニタに集中して形式検証を適用するアプローチを採用しています。

本発表では、その最初のステップとして、参照モニタに対する時差攻撃(Time-Of-Check-To-Time-Of-Use: TOCTTOU)を防止するために、自動検証コード生成と並列検証を用いた二段階の検証により、現実的なコストで参照モニタのセキュリティを強化することを目指しています。