PSec: Programming Secure Distributed Systems using Enclaves
TL;DR
セキュアな分散システムを構築するためのステートマシンベースのプログラミング言語(ベースはP言語)
悪意のある分散ホストから保護するために、SGXを活用したセキュアな分散サンドボックスを実現
既存のSGXプログラミングと比べて安全な分散アプリケーションを比較的に簡単に実装可能
本文
https://gyazo.com/7ffd9a08b6dd3f66bcb930125e59e079
主要な構成要素(言語レベル)
Machine
ステートマシン
イベントの送受信とステートを管理
新しいSSMないしUSMを作成可能
Secure State Machine(SSM)
Untrusted State Machine(USM)
Event
ステートマシンは、イベントを非同期に送信することで相互に通信
Trusted Event(信頼できる世界から発信された悪意のないペイロードを含む)
機密/信頼されたデータが含まれる
Untrusted Event(信頼できない世界から発信された破損/不正なペイロードを含む可能性がある)
Sealing
Intel SGX SDKのシーリング機能を用いてSSM内のデータを暗号化(seal)し、特定のSSMのインスタンスのみが復号化(unseal)できるようにすることが可能
Local Authentication
USMは同じ分散ホスト上で実行されているSSMが実際に有効なコードを実行しているかどうかを確認可能
USMから特定のSSMへの一方的な信頼を確立するため(SSM同士の信頼はすでに確立されている)
PSec Type Checker
Event送受信時に静的な型チェックを行う。これによって情報フロー制御を実現
2種類のセキュリティラベル(H/High, L/Low)
例: Trusted EventにはHラベルのデータしか含まれない。Trusted SendはHラベルのデータしか送信できないなど
システムアーキテクチャ
https://gyazo.com/e236c77644d924dcfcc476c7391bd77e
KPS(Key Provisioning Server)
システム内に存在する全てのSSMの信頼の根源
全てのSSMのIP Address, Identity, Capabilityなどの情報を持つ
このシステムにおいて絶対信頼しないといけない存在
KPSの公開鍵はすべてのEnclaveに組み込まれている
単一障害点
PSec Secure Runtime
Enclave内でのSSMの実行を担当
Enclaveごと1SSM
PSec Untrusted Runtime
USMを担当
ネットワークにメッセージを送信
プロトコル
前提として本システムはKPSと最初のSSMは信頼できる(絶対信頼する必要がある)存在としている
bootstrap node的な感じ
最初のSSMを起点にSSMを増やしていく(trust chain)。SSMは自分が作ったSSMを信頼し、作られたSSMは自分を作ってSSMを信頼。また、信頼されている仲間のSSMが信頼できると判断したSSMを追加で信頼
Identity: 公開鍵と秘密鍵のペア。ステートマシン認証用
Capability: 公開鍵と秘密鍵のペア。Event送受信時の認証用
Secure Sigma* Channel
EnclaveとKPSの間で疎通するためのセキュアなチャネル
Intel SGXのSigmaプロトコル(SGX SDKで提供される認証済みDiffie-Hellmanのバージョン)を用いて作成
SSMのEnclave検証
https://gyazo.com/73b830c7dc7cbe8256926980fa60c12e
新しいSSM作成フロー(SSM1は親、SSM2は子。SSM1がSSM2を作成)
1. SSM1はKPSから生成したいSSM2のIP Addressを取得
2. SSM1はcreateMacineRequest()を実行。この際、SSM1のIdentity公開鍵と作成するSSMタイプを指定
3. Host Machine2でSSM2が作成され(Enclave作成 -> PSecプロセス初期化 -> SSM2作成 -> Identity生成)、KPSとSecure Sigma* ChannelでSSM1のIdentity公開鍵、SSM2のIndentity公開鍵、作成するSSMタイプを送信
4. KPSはSSM2のCapabilityを生成し、保存とともにSSM2に生成されたCapabilityを返す
5. SSM2はSSM1に対して自分のIdentity公開鍵を返す
6. SSM1はKPSとSecure Sigma* ChannelでSSM1のIdentity公開鍵、SSM2のIdentity公開鍵、作成するSSMタイプを送信
7. KPSはSSM1に対してSSM2のCapabilityを返す
親SSMがKPSからCapabilityを正常に取得した場合、KPSはこのCapabilityを生成する前にSecure Sigma*プロトコルを使用して子Enclaveを検証するため、子SSMが安全に作成されたことが保証される。また、子SSMは、KPSの検証により、親SSMのみがCapabilityを受け取ることが保証される
Eventのやりとり(SSM1からSSM2に機密データが含まれているEventを送信するフロー)
前提としてSSM1は、SSM2のCapabilityとIdentity公開鍵を持っている
1. SSM1からEvent送信処理実行
2. Eventペイロードをシリアル化
3. SSM2のCapability秘密鍵で署名
jkcomment.icon え?
jkcomment.icon あ、future workとなっているのか
4. SSM2のIdentity公開鍵で暗号化されたセッションキーでEventと署名を暗号化し、送信
5. SSM2は送られてきたEventが信頼できるSSMかどうかを確認し、Eventを復号化
送信されるデータがこの送信プロセスを通じて信頼されていない世界に漏れることはなく、信頼されたSSMから意図されたSSMに送信されることを保証
参考
マイクロソフトとカリフォルニア大学バークレー校が開発した非同期イベント駆動型プログラミング言語
組み込みシステム、ネットワークで結ばれたシステム、分散システムといった非同期システムにおける構成要素間の通信をモデル化するドメインに特化
コンパイルすると実行可能なCコードが生成される
事例
Windows 8のUSB 3.0ドライバー
Amazon Web Servicesの内部で使われている
Appendix
関連研究
Jif/split, SIF, Swift, Fabric
言語ベースの情報フロー制御を利用して,システムを通過するデータに機密性と完全性のポリシーを適用する
Verifiable Confidential Cloud Computing(VC3)
エンクレーブを用いて安全な分散計算を可能にする
MapReduceのケースに限定されており、一般的なアプリケーションには合わせられていない
Ryoan
悪意のある分散ホストから保護するために、SGXを活用したセキュアな分散サンドボックスを作成
機密データ送信のための様々なセキュアプロトコルを設計し、様々なアプリケーションを実装しているが、言語ベースのアプローチではない
分散システム
分散システムとは、ネットワークで接続された複数のコンピュータから構成されるシステム。複数のコンピュータに作業を分担させて稼働させることで、各コンピュータにかかる負荷を分散させることができ、安定した処理をさせることが可能