学内研究所等 【 表示 ／ 非表示 】

学内研究所等 【 表示 ／ 非表示 】

• 2020年

  -

  2022年

  理工学術院総合研究所   兼任研究員

学歴 【 表示 ／ 非表示 】

学歴 【 表示 ／ 非表示 】

• 2000年09月

  -

  2006年08月

  カリフォルニア大学バークレー校   電子工学・コンピュータサイエンス学科   コンピュータサイエンス専攻  

• 1996年09月

  -

  2000年05月

  コロンビア大学   工学・応用科学科   コンピュータサイエンス専攻  

学位 【 表示 ／ 非表示 】

学位 【 表示 ／ 非表示 】

• コロンビア大学   学士

• カリフォルニア大学バークレー校   修士

• カリフォルニア大学バークレー校   博士

経歴 【 表示 ／ 非表示 】

経歴 【 表示 ／ 非表示 】

• 2017年09月

  -

  継続中

  早稲田大学   理工学術院 基幹理工学部 情報理工学科   教授

• 2014年04月

  -

  2017年09月

  北陸先端科学技術大学院大学   情報科学研究科   教授

• 2011年04月

  -

  2014年03月

  名古屋大学   大学院情報科学研究科   准教授

• 2007年01月

  -

  2011年03月

  東北大学   大学院情報科学研究科   助教

所属学協会 【 表示 ／ 非表示 】

所属学協会 【 表示 ／ 非表示 】

• 　

  　

  　

  ACM

• 　

  　

  　

  情報処理学会

• 　

  　

  　

  ソフトウェア科学会

研究分野 【 表示 ／ 非表示 】

研究分野 【 表示 ／ 非表示 】

• 情報学基礎論

• ソフトウェア

研究キーワード 【 表示 ／ 非表示 】

研究キーワード 【 表示 ／ 非表示 】

• プログラミング言語

• プログラム検証

• プログラム合成

• 型システム

• 自動定理証明

全件表示 >>

論文 【 表示 ／ 非表示 】

論文 【 表示 ／ 非表示 】

• Bucketing and Information Flow Analysis for Provable Timing Attack Mitigation

  Tachio Terauchi, Timos Antonopoulos

  Journal of Computer Security   28 ( 6 ) 607 - 634  2020年  [査読有り]

• Failure of Cut-Elimination in Cyclic Proofs of Separation Logic

  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

  Computer Software   37 ( 1 ) 1_39 - 1_52  2020年  [査読有り]  [招待有り]  [国内誌]

  　概要を見る

  <p>This paper studies the role of the cut rule in cyclic proof systems for separation logic. A cyclic proof system is a sequent-calculus style proof system for proving properties involving inductively defined predicates. Recently, there has been much interest in using cyclic proofs for proving properties described in separation logic with inductively defined predicates. In particular, for program verification, several theorem provers based on mechanical proof search procedures in cyclic proof systems for separation logic have been proposed. This paper shows that the cut-elimination property fails in cyclic proof systems for separation logic in several settings. We present two systems, one for sequents with single-antecedent and single-conclusion, and another for sequents with single-antecedent and multiple-conclusions. To show the cut-elimination failure, we present concrete and reasonably simple counter-example sequents which the systems can prove with cuts but not without cuts. This result suggests that the cut rule is important for a practical application of cyclic proofs to separation logic, since a naïve proof search procedure, which tries to find a cut-free proof, gives a limit to what one would be able to prove.</p>

  DOI CiNii

• Games for Security under Adaptive Adversaries.

  Timos Antonopoulos, Tachio Terauchi

  In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF 2019)     216 - 229  2019年  [査読有り]  [国際誌]

  DOI

• A Formal Analysis of Timing Channel Security via Bucketing.

  Tachio Terauchi, Timos Antonopoulos

  In Proceedings of the 8th International Conference on Principles of Security and Trust (POST 2019)     29 - 50  2019年  [査読有り]  [国際誌]

  DOI

• A Fixpoint Logic and Dependent Effects for Temporal Property Verification.

  Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)     759 - 768  2018年  [査読有り]  [国際誌]

  DOI

全件表示 >>

受賞 【 表示 ／ 非表示 】

受賞 【 表示 ／ 非表示 】

• 早稲田大学リサーチアワード 国際研究発信力

  2019年12月   早稲田大学  

  受賞者： 寺内 多智弘

• The EASST Award for the Best ETAPS Paper Related to the Systematic and Rigorous Engineering of Software and Systems.

  2017年04月   European Association for Software Science and Technology   Nominee  

  受賞者： Arthur Blot, Masaki Yamamoto, Tachio Terauchi

• 発表賞(一般)

  2008年03月   ソフトウェア科学会 第10回プログラミングおよびプログラミング言語ワークショップ (PPL 2008)  

  受賞者： 寺内 多智弘

• 第4回野口研究奨励賞

  2008年   情報処理学会 東北支部  

  受賞者： 寺内 多智弘

共同研究・競争的資金等の研究課題 【 表示 ／ 非表示 】

共同研究・競争的資金等の研究課題 【 表示 ／ 非表示 】

• 数理論理手法と人工知能手法の融合に基づくマルウェアの自動意味理解

  挑戦的研究(開拓)

  研究期間:

  2020年07月

  -

  2026年03月

   

  小川 瑞史, NGUYEN MinhLe, 寺内 多智弘, 関 浩之

• 時相的・関係的仕様からの高レベルプログラム合成

  基盤研究(B)

  研究期間:

  2020年04月

  -

  2025年03月

   

  海野 広志, 南出 靖彦, 寺内 多智弘

• 高階・再帰的データ構造への破壊的代入を含む高レベル言語プログラムの高精度な検証

  基盤研究(B)

  研究期間:

  2017年04月

  -

  2022年03月

   

  寺内 多智弘, 海野 広志

  　概要を見る

  依存型・依存エフェクトシステムと一階述語不動点論理(first-order fixpoint logic)による高階プログラムの時相論理仕様検証に関する研究を行った。研究の成果をまとめた論文は理論計算機科学分野におけるトップ国際会議LICS 2018に採録された。また、関連して、一階述語不動点論理式の真偽性を解く自動定理証明アルゴリズムの研究および一階述語不動点論理による双模倣性の検証などのについても研究を推進し、The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018)およびThird Workshop on Mathematical Logic and its Applications (MLA 2019)にてこの研究に関する講演を行った。
  <BR>
  また、循環証明(cyclic proof)と分離論理(separation logic)に関する研究も行った。具体的には、循環証明による分離論理の定理証明は、再帰データ構造を含む場合カット除去不可能であることを示した。この研究に関してThe 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)、日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)およびMLA2019にて講演を行った。
  <BR>
  加えて、サイドチャネル攻撃に対する耐タンパ性の検証など情報セキュリティに関するプログラム検証の研究を行った。

• サイドチャネル攻撃耐タンパ性のためのプログラム検証・プログラム合成技術

  挑戦的研究(萌芽)

  研究期間:

  2018年06月

  -

  2021年03月

   

  寺内 多智弘

  　概要を見る

  代表的なサイドチャネル攻撃の一つであるタイミング攻撃に関する研究を行った。具体的には、bucketingというプログラム変換によるタイミング攻撃に対する防衛手法について研究を行った。この研究ではどのようなプログラムおよび攻撃者に対してbucketingが有効であるのか調査することを目指し、bucketingにより安全性の保証を得るための必要条件および十分条件に関する成果を得た。これら、必要条件・十分条件は解析対象システムの正規チャネルとサイドチャネルの安全性を分離して議論することを可能とする枠組みであり、また、過去の観測に依存した動作を行える強力なadaptiveな攻撃者を考慮している。この研究の成果をまとめた論文はセキュリティに関する国際会議The 8th International Conference on Principles of Security and Trust (POST 2019)に採録された。
  <BR>
  加えて、一階述語不動点論理による時相仕様検証や循環証明による分離論理のための定理証明など、関連するより一般的なプログラム検証および定理証明についての研究も行った。

• 数理論理学とその応用の国際研究拠点形成

  研究期間:

  2015年04月

  -

  2020年03月

   

  石原 哉

全件表示 >>

講演・口頭発表等 【 表示 ／ 非表示 】

講演・口頭発表等 【 表示 ／ 非表示 】

• Inferring Simple Strategies for Efficient Quantified SMT Solving (Poster Presentation)

  Souta Yamauchi, Tachio Terauchi

  17th Asian Symposium on Programming Languages and Systems (APLAS 2019)  

  発表年月： 2019年12月

• A Fixpoint Logic and Dependent Effects for Temporal Property Verification

  Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi  [招待有り]

  Dagstuhl Seminar 19371: Deduction Beyond Satisfiability  

  発表年月： 2019年09月

• Solving First-Order Fixpoint Logic for Program Verification

  Takashi Nishikawa, Yuki Satake, Yoji Nanjo, Hiroshi Unno, Naoki Kobayashi, Tachio Terauchi, Eric Koskinen  [招待有り]

  Third Workshop on Mathematical Logic and its Applications (MLA 2019)  

  発表年月： 2019年03月

• On Cut-Elimination Theorem in Cyclic-Proof Systems

  Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome

  Third Workshop on Mathematical Logic and its Applications (MLA 2019)  

  発表年月： 2019年03月

• Failure of Cut-Elimination in Cyclic Proofs of Separation Logic

  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

  ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）  

  発表年月： 2019年03月

全件表示 >>

現在担当している科目 【 表示 ／ 非表示 】

現在担当している科目 【 表示 ／ 非表示 】

• 情報通信基礎　【前年度成績S評価者用】

  基幹理工学部

  2021年   春学期

• 情報通信基礎

  基幹理工学部

  2021年   春学期

• プロジェクト研究Ｂ

  基幹理工学部

  2021年   秋学期

• 情報理工学実験Ｃ 【前年度成績S評価者用】

  基幹理工学部

  2021年   秋学期

• 情報理工学実験Ａ　【前年度成績S評価者用】

  基幹理工学部

  2021年   秋学期

全件表示 >>

委員歴 【 表示 ／ 非表示 】

委員歴 【 表示 ／ 非表示 】

• 2020年04月

  -

  継続中

  ソフトウェア科学会 プログラミング論研究会  運営委員

• 2018年04月

  -

  継続中

  情報処理学会プログラミング研究会(PRO)  幹事

• 2021年

  -

  2022年

  The 35th IEEE Computer Security Foundations Symposium (CSF 2022) Program Committee  Program Committee

• 2021年

  -

  2022年

  37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)  Program Committee

• 2021年

  -

  2022年

  49th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2022)  Program Committee

全件表示 >>