takibi

Takibiは、カスタムシステム言語とそれに対応するモノリシックカーネルからなる研究プロトタイプです。このプロジェクトは、バッファオーバーフロー、リソースリーク、コンテキスト違反などの一般的なカーネルレベルの障害を、型システムに直接エンコードすることで排除することを目的としています。 主な技術的特徴は以下の通りです： - 言語設計：証明済み配列インデックスのためのリファインメント型、リソース管理のためのアフィンおよび線形所有権、そして実行コンテキスト（例：ブロッキング vs 割り込みコンテキスト）を追跡するためのエフェクトシステムを実装しています。 - コンパイラ：OCamlで記述されており、ネイティブコード生成にLLVM 19を利用しています。 - カーネル機能：Linux-ABI互換であり、既存のAArch64 ELFバイナリを実行可能です。Linuxシステムコールのサブセット、オンデマンドで拡張されるページテーブル、コピーオンライト、およびext2ルートファイルシステムをサポートしています。 - ネットワーキング：ARP、IPv4/IPv6、ICMP、TCPをサポートする独自のTCP/IPスタックを備えています。 - ハードウェアサポート：QEMU/AArch64およびRaspberry Pi 5で起動し、Alpine BusyBoxの実行やHTTPdによるファイル提供が可能です。 このプロジェクトは、実行時のトラップから静的な正しさの証明へと移行し、言語をどのように進化させれば現実世界のシステムプログラミングの問題を解決できるかを探求するための研究手段として機能します。