Rust言語でファームウェア、OS、言語処理系を実装して、CSS 2020で発表した

先月、国内最大のセキュリティ研究会であるコンピュータセキュリティシンポジウム 2020(CSS 2020)が開催され、そこで、Rust言語を用いてファームウェア、OS、言語処理系を設計・実装した話を発表しました。本来、CSS 2020はリアルで開催されるはずでしたが、コロナ禍の影響でオンライン開催となり発表動画作成が求められました。せっかく作った動画をこのまま捨て置くのももったいないと思い、ここで供養したいと思います。

 

www.youtube.com

概要

内容は、Rust言語を用いて、AArch64のセキュアワールド内で動作するファームウェア、OS、プログラミング言語処理系を実装した話となります。と言っても、まだまだ基本的な部分しか実装しておらず、実現目標に対して2〜3割と言ったところですが、どうぞご笑覧ください。

ブート部分は多少アセンブリ言語を使っていますが、その他の部分はRustでフルスクラッチで実装しています。修正したい箇所も多く残っていますが、まだまだ出来ていません。

対応ハードウェアは、今のところPine64+のみでUSBケーブルからのブートが必要ですが、機能縮小板はQemuのRaspi3エミュレーションで動作します。

言語処理系

言語処理系はまぁまぁ凝っており、構文はLispっぽく、型システムはOCamlHaskellっぽく設計・実装しています。ですので、代数的データ型、末尾呼び出し最適化、ジェネリクス型推論、パターンマッチなどの機能が利用できます。ただし、高カインド型は未対応のため、モナドは使えません。型システムは形式的に定義しているため、検証もしやすいと思います(手をつけられていませんが…)。

さらに、効果系と呼ばれる機能を適用しているため、副作用のある関数と、そうでない関数を完全に分離可能になり、安全にセキュアワールド内へプログラムを注入することができます。本当はRustとの連携をもっと強固にしたいところですが、まだ実現できておらず、今後の予定となっています。

 

なお、ソースコードオープンソースライセンスで公開しており、以下より取得できます。

GitHub - ytakano/baremetalisp

GitHub - ytakano/blisp

もう少し時間があれば設計や実装も進めることができそうですが、大学はやたら忙しく、日々ワード、エクセルと格闘しているため、最近はあまり進捗はありません。今の担当講義が終わったら、また時間を見つけて研究を進めたいところです。