メンバー: Pierre-Louis Aublin
カテゴリー: Innovating
ユーザーのためのインターネット: セキュアで検証可能かつ信頼性のあるシステムの構築
背景
“インターネットの可能性は無限大です。世界的資源として、インターネットは商取引、レクリエーション、研究、教育、エンターテイメントなど、あらゆることを支えています。しかし、さまざまな利害関係者やネットワークの競合する要求がある中で、インターネットの未来を守ることは不可能に思えることがあります。” — インターネットソサエティ
今日のインターネットは、セキュリティ、信頼性、ユーザーデータを管理し、ユーザーに自律性を放棄させる中央集権的で不透明なプラットフォームによって支配されています。これは、ユーザーが自らのデータや選択、システムへのアクセスのタイミングを制御することを放棄することを意味します。
単一の仲介者(例えばクラウドサービスプロバイダー)1やAS2での技術的失敗が、広範なインターネットの一部を利用不可にすることがあるだけでなく、さまざまなインターネット関連者(クラウドプロバイダー、ISPなど)が、商業的利益3、国家監視4、悪意のあるトラフィック操縦5のためにインターネットユーザーの信頼を日常的に利用しています。
目的
このプロジェクトは、インターネットの関係者からそのユーザーに焦点を移し、システムがセキュアで検証可能、かつ信頼性があるインターネットを構築することを目指しています。これにより、人々は独占企業や不透明なプラットフォームに自律性を譲ることなく、テクノロジーを利用できるようになります。
これにより、ユーザーは実用性を犠牲にせずに以下を行えるようになります:
- 自分のデータや秘密を保護する。
- システムの挙動を検証する。
- 障害があってもオンラインサービスにアクセスする。
- ユーザーのロックインを避けて代替システムを使用する。
アプローチ
私たちのアプローチは、以下の技術的柱に基づいています:
- 信頼よりも保証: フォーマル検証(TLA+6、Verus7、Flux8など)を使用して、システムが正しいことを証明し9、セキュリティとプライバシーの保証を得るためのTrusted Execution Environments10,11を活用します。
- 信頼性: 故障耐性12とレジリエンス13を実装して、失敗を防ぎ、回復します。
- コンポーザビリティ: ユーザーのロックインを避け、小さく検証可能なコンポーネントをレゴブロックのように構築し、失敗したり侵害されたコンポーネントを簡単に隔離できるようにします14,15。
- 実用性: レジリエンスとセキュリティは、実用性を犠牲にすることなく実現されるべきです。システムがあまりにも複雑または遅い場合、それは回避されるか、放棄されるでしょう16。したがって、私たちはレジリエントでセキュアなだけでなく、受け入れ可能なパフォーマンスを提供するシステムを構築することを目指しています17。
現在の研究方向
ユーザーのインターネットセキュリティの保証
今日のセキュリティはしばしば幻影です:ユーザーはプラットフォーム、OS、またはハードウェアを「信頼」しますが、自分のデータが安全で改ざんされていないかを簡単に検証することはできません。
私たちは、強力な攻撃者からコードやデータを保護するプロセッサ内の安全な領域であるTrusted Execution Environmentsを活用して、ユーザーのデータを保護し、プラットフォームが何をしているのかに関する保証を提供するシステムを構築します。これには、サーバーレスコンピューティングを機密かつ実用的にし、ユーザーの入力をキー入力記録ソフトやマルウェアから保護すること、あるいは強力なセキュリティ保証を提供する新しいTrusted Execution Environmentsを設計することが含まれます。
ビザンチン障害耐性の採用改善
障害耐性、特にビザンチン障害耐性(BFT)は、任意の障害(クラッシュ、構成エラー、悪意のある攻撃者など)があっても継続的な機能を保証しますが、追加のリソースや複雑な通信メカニズムを必要とし、採用を妨げる無視できないパフォーマンスオーバーヘッドを加えます。
私たちは、パフォーマンス、レジリエンス、または使いやすさを損なうことなく、障害耐性を実現するための新しいソリューションを開発しています:
- Trusted Execution EnvironmentsやスマートNICを統合することで、ユーザーまたは開発者の視点から見て、これらのプロトコルをより透明にする。
- システムの堅牢性を損なわないパフォーマンス最適化を慎重に導入する。
普及活動
(完全なリストは こちら で確認できます。)
ブログ記事
- “LLM推論のための故障耐性”。IIJエンジニアリングブログ。2024年12月。
- “フェイクニュースと闘うための信頼できる写真を目指して”。IIJエンジニアリングブログ。2024年7月。
- “ハードウェアのタイムスタンプを使用してネットワークの待ち時間を測定する方法”。IIJエンジニアリングブログ。 2023年10月。
プレゼンテーション
- 2025年6月、フランスのグルノーブル市でVMPSec ’25ワークショップを共同開催。
- 2025年5月、IIJLabセミナーでサーバーレス機密VMに関する進行中の作業を発表。
- 2024年9月、FAUエアランゲン、ミュンヘン工科大学、ロイヤル・ホロウェイ大学、インペリアル・カレッジ・ロンドンで発表。
科学的出版物
- “A Case for Unifying Trusted Execution Environments”, Pierre-Louis Aublin, Thomas Prévost, Hajime Tazaki, and Kuniyasu Suzaki, HAP ’26 workshop (co-located with DSN ’26), June 2026.
- “What You See Is Not What You Get: Introducing the Trusted Camera Framework to Combat Fake News”, Pierre-Louis Aublin, DASC ’25 conference, October 2025.
- “BFTaaS: Byzantine Fault Tolerance as a Service through NIC-Level Aggregation”. Rui Wang, Arne Vogel and Pierre-Louis Aublin, DASC ’25 poster, October 2025.
- “Mitigating Cryptographic Bottlenecks of Low-latency BFT Protocols”, Pierre-Louis Aublin and Arne Vogel, DAIS ’25 conference. June 2025
- “Transparent Management of BFT Systems with TEE”. Bijun Li, and Pierre-Louis Aublin. In Proceedings of the 6th Workshop on System Software for Trusted Execution (SysTEX 2023). May 2023.
- “Easy-to-Adopt and Bottleneck-free Byzantine Fault Tolerant Protocols”. Pierre-Louis Aublin. In the 17th Asian Internet Engineering Conference (AINTEC). December 2022.
- “Towards TEEs with Large Secure Memory and Integrity Protection Against HW
Attacks”. Pierre-Louis Aublin, Mohammad Mahhouk, and Ruediger Kapitza. In the
5th Workshop on System Software for Trusted Execution (SysTEX 2022). March
ソフトウェア
- “Mitigating Cryptographic Bottlenecks of Low-latency BFT Protocols” 論文の コードアーティファクト
お問い合わせ
これらのプロジェクトにご興味がおありの場合、またはご質問がある場合は、遠慮なくご連絡ください。
O’Flaherty, K. Cloudflare Down—New Outage Takes Internet Down, Again. Forbes (2025).↩︎
Sharma A. Major BGP leak disrupts thousands of networks globally. Bleeping Computer (2021).↩︎
Thomas, K. et al. Ad injection at scale: Assessing deceptive advertisement modifications. IEEE Symposium on Security and Privacy (2015).↩︎
NSA Stops Certain Section 702 “Upstream” Activities. NSA (2017).↩︎
Birge-Lee, H. et al. Bamboozling certificate authorities with BGP. USENIX Security Symposium (2018).↩︎
Lamport, L. Specifying systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley (2002).↩︎
Lattuada, A. et al. Verus: A Practical Foundation for Systems Verification. ACM SOSP (2024).↩︎
Lehmann, N. et al. Flux: Liquid types for rust. ACM PLDI (2023).↩︎
Hawblitzel, C. et al. IronFleet: Proving Practical Distributed Systems Correct. ACM SOSP 2015.↩︎
Costan, V. and Devadas, S. Intel SGX Explained, IARC Cryptology (2016).↩︎
Misono, M. et al. Confidential VMs explained: An empirical analysis of AMD SEV-SNP and Intel TDX. ACM POMACS 8.3: 1-42 (2024).↩︎
Castro, M. and Liskov, B. Practical Byzantine Fault Tolerance. Usenix OSDI (1999)↩︎
Ergenc D. et al. Resilience in Edge Computing: Challenges and Concepts. 5), Foundations and Trends in Networking 14:4: 254-340 (2025).↩︎
Ferraiuolo, A. et al. Komodo: Using verification to disentangle secure-enclave hardware from software. ACM SOSP (2017).↩︎
Sartakov, V. et al. Spons & Shields: practical isolation for trusted execution. ACM VEE (2021).↩︎
Saltzer, J. and Schroeder, M. The protection of information in computer systems. IEEE journal 63:9, 1278-1308 (1975).↩︎
Lampson B. Hints for computer system design. ACM SOSP (1983).↩︎
