Workshop on Software, Architecture, and Theory for Secure Systems

セキュアシステムのためのソフトウェア、アーキテクチャ、理論に関するワークショップ (SATSS)

趣旨

FPGAの普及、オープンソースの充実によりRISC-Vに代表されるような計算機システムが容易に作れるようになりました。計算機理論分野では現実社会に応用する研究が活発化しAWSなどでは実システムに供しています。一方で新しい原理を理論研究と共に計算機ハードウェアからソフトウェアのレイヤまで研究・開発するために必要な知識の獲得と議論の場が乏しいと我々は考えています。そこで、若手研究者・技術者の方々が学び議論できる場を設けることにしました。


世話人

  • 関山 太朗（NII／ROIS）
  • 大畑 幸矢 (ROIS)
  • 畑 輝史（慶應義塾大学）

Keywords

  • TEE, Confidential Computing, Hypervisor, VM
  • Formal Verification, Theorem Prover, SAT/SMT Solver
  • RISC-V, Linux, Rust, ProVerif, Tamarin

対象

  • 学生、若手研究者・技術者、教育関係者

形式

  • 当初は勉強会的に参加者の中から有志が発表し全員で議論。皆さんとの議論を大事にしたいので原則現地参加をお願いします。
  • 科研費における若手の定義は学位取得後8年未満の研究者としていますが、この定義にとらわれず、ここでは「若手」とは年齢問わず自らの自由な発想の元、研究・開発している・していきたい方々とします。
  • 企画・運営していく若手ボランティアも募集しています。第1回ワークショップ参加登録フォームにご記入ください。

今後の開催予定

  • 第9回：理論関連のトピック（具体的な内容は調整中）
    話者：大堀 淳（ROIS／東北大学），他調整中
    日時：2025年8月ごろ
    開催場所：未定
  • 第10回：システムソフトウェア関連のトピック（具体的な内容は調整中）
    話者：光来 健一（九工大），他調整中
    日時：2025年10月ごろ
    開催場所：未定
  • 第11回：ハードウェア関連のトピック（具体的な内容は調整中）
    話者：内山 一秀（ROIS），他調整中
    日時：2025年12月ごろ
    開催場所：未定
  • 第12回：未定
    話者：未定
    日時：2026年3月ごろ
    開催場所：未定

終了したワークショップ

  • 第8回："Cloud Server Security: From Trusted Execution Environment (TEE) to Fully Homomorphic Encryption (FHE)"
    話者：Yan Solihin
    日時：2025年6月3日(火)16:30〜18:30
    開催場所：早稲田大学グリーン・コンピューティング・システム研究開発センター (40号館) 1階プレゼンテーションルーム
    概要
    In this talk I will discuss the ongoing challenges for ensuring the confidentiality and integrity of computation in the cloud servers. In the first part of the talk, I will discuss the drawbacks of current Trusted Execution Environment (TEE) designs. TEE protects sensitive applications in the cloud with the minimal trust in the cloud provider. Existing TEEs with integrity protection however lack support for data management primitives, causing data sharing between enclaves either insecure or cumbersome. This paper proposes a new data abstraction for TEEs, data enclave. As a data-centric abstraction, data enclave is decoupled from an enclave’s existence, is equipped with flexible secure permission controls, and crytographically isolated. It eliminates the hurdles for enclaves to cooperate efficiently, and at the same time, enables dynamic shrinking of the height of integrity tree for performance. This paper presents this new abstraction, its properties, and the architecture support. Experiments on synthetic benchmarks and three real-world applications all show that data enclave can help improve the efficiency of enclaves and inter-enclave cooperations significantly while enhancing the security protection. In the second part of the talk, I will discuss our research in Fully Homomorphic Encryption (FHE) verifiability. FHE allows computations to be performed directly on encrypted data without needing to decrypt it first. This “encryption-in-use” feature is crucial for securely outsourcing computations in privacy-sensitive areas such as healthcare and finance. Nevertheless, in the context of FHE-based cloud computing, clients often worry about the integrity and accuracy of the outcomes. This concern arises from the potential for a malicious server or server-side vulnerabilities that could result in tampering with the data, computations, and results. Ensuring integrity and verifiability with low overhead remains an open problem, as prior attempts have not yet achieved this goal. To tackle this challenge and ensure the verification of FHE’s private computations on encrypted data, we introduce DataSeal, which combines the low overhead of the algorithm-based fault tolerance (ABFT) technique with the confidentiality of FHE, offering high efficiency and verification capability. Through thorough testing in diverse contexts, we demonstrate that DataSeal achieves much lower overheads for providing computation verifiability for FHE than other techniques that include MAC, ZKP, and TEE. DataSeal’s space and computation overheads decrease to nearly negligible as the problem size increases.
  • 第7回：TEE関連研究動向
    日時：2024年7月1日(月)14:00〜17:00
    共催：早稲田大学グリーン・コンピューティング・システム研究機構
    開催場所：早稲田大学グリーン・コンピューティング・システム研究開発センター (40号館) 1階プレゼンテーションルーム
    　　　　　リモート参加可能（開催前日にメールでURLを送付）
    定員：60名
    話題：
    　"CTR: Checkpoint, Transfer, and Restore for Secure Enclaves"
    　　　Yoshimichi Nakatsuka (ETH Zurich)
    　"TDOS: Trustworthy Heterogeneous Disaggregated Architectures"
    　　　Atsushi Koshiba (Technical University of Munich)
    　"OP-TEEの利用事例：OP-TEEを用いたIoTのための安全な階層鍵管理機構"
    　　　竹房 あつ子 (NII)
  • 第6回：Arm TrustZone
    日時：2024年5月10日(金)13:00〜18:00
    　　　セコムIS研究所とデータセンター見学：13:00〜15:30
    　　　　　(企業の方は見学出来ません)
    　　　Arm TrustZone講義：15:30〜18:00
    共催：セコム（株）
    開催場所：セコムIS研究所
    　　　　　リモート参加可能（開催前日にメールでURLを送付）
    講師：宮澤慎一（セコム（株））
    概要：
    　　1) ARMとTrustZoneの概要
    　　2) Global Platformの概要
    　　3) OP-TEEの解説
    　　4) OP-TEEプログラミングハンズオン
    ハンズオンではQEMUを使います。ノートPCをご持参ください。あらかじめソフトウェアをインストールしておいてください。詳細は追って連絡します
    定員：100名（見学は30名）
  • 第4回&第5回：形式検証入門、メモリ暗号化・整合性検証の最近動向
    日時：2024年3月8日(金)15:00〜18:00
    共催：早稲田大学グリーン・コンピューティング・システム研究機構
    開催場所：早稲田大学グリーン・コンピューティング・システム研究開発センター (40号館) 1階プレゼンテーションルーム
    　　　　　リモート参加可能（開催前日にメールでURLを送付）
    講師：関山太朗（国立情報学研究所）
    　　　高前田伸也（東京大学）
    定員：60名
  • 第3回：Virtualization 最近動向 RISC-V Virtualization, Intel TDX, Arm CCA
    日時：2024年2月1日(木)16:00〜18:00
    開催場所：国立情報学研究所 1208-1210会議室
    　　東京都千代田区一ツ橋2-1-2 学術総合センター12階
    講師：河野健二 （慶大）
    定員：60名
  • 第2回：RISC-Vの最近動向 WorldGuard, IOMMUを中心に
    日時：2024年1月29日(月)13:30〜15:30
    共催：早稲田大学グリーン・コンピューティング・システム研究機構
    開催場所：早稲田大学グリーン・コンピューティング・システム研究開発センター (40号館) 1階プレゼンテーションルーム
    講師：木村啓二（早大）
    定員：60名
  • 第1回：TEEの概要 RISC-V PMPを中心に
    日時：2023年12月18日(月)17:00〜19:00 (会場は20:00まで)
    開催場所：東京大学理学部7号館007号室(地下)(会場を変更しました)
    講師：須崎有康（情セ大）
    定員：50名

発起人

  • 代表：石川裕（NII/ROIS）
  • システムソフトウェア：河野健二 （慶大）、光来健一（九工大）、須崎有康（情セ大）、合田憲人（NII/ROIS）、竹房あつ子（NII）
  • アーキテクチャ：木村啓二（早大）、高前田伸也（東大）、塩谷 亮太（東大）、五島正裕（NII）