2024/12/21 更新

写真a

テラウチ タチオ
寺内 多智弘
所属
理工学術院 基幹理工学部
職名
教授
学位
博士 ( カリフォルニア大学バークレー校 )
修士 ( カリフォルニア大学バークレー校 )
学士 ( コロンビア大学 )
プロフィール

プログラミング言語分野の研究を行っています。特に、プログラムの正しさを正式かつ(できるだけ)自動的に検証する「プログラム検証」や正しいプログラムを自動生成する「プログラム合成」の研究、およびプログラム検証・合成技術のセキュリティへの応用に興味があります。加えて、型システム、数理論理学と(特に自動)定理証明、形式言語理論とオートマトン理論など基礎理論・基礎アルゴリズムに関する研究も行っています。

経歴

  • 2017年10月
    -
    継続中

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

  • 2014年04月
    -
    2017年09月

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

  • 2011年04月
    -
    2014年03月

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

  • 2007年01月
    -
    2011年03月

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

学歴

  • 2000年09月
    -
    2006年08月

    カリフォルニア大学バークレー校   Department of Electrical Engineering and Computer Sciences   Computer Science Division  

  • 1996年09月
    -
    2000年05月

    コロンビア大学   School of Engineering and Applied Science   Computer Science Major  

委員歴

  • 2024年
    -
    2025年

    The 32nd ACM SIGSAC Conference on Computer and Communications Security (CCS 2025)  Program Committee

  • 2024年
    -
    2025年

    The 37th International Conference on Computer Aided Verification (CAV 2025)  Program Committee

  • 2024年
    -
    2025年

    ソフトウェア科学会 第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025))  プログラム委員

  • 2024年
    -
    2025年

    The 40th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2025)  Program Committee

  • 2024年
    -
    2025年

    The 52nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2025)  Program Committee

  • 2024年
    -
    2025年

    The 38th IEEE Computer Security Foundations Symposium (CSF 2025)  Program Committee

  • 2020年04月
    -
    2024年03月

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

  • 2023年
    -
    2024年

    The 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2024)  Program Committee

  • 2023年
    -
    2024年

    The 24th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2024)  Program Committee

  • 2023年
    -
    2024年

    The 45th ACM SIGPLAN Symposium on Programming Language Design and Implementation (PLDI 2024)  Program Committee

  • 2023年
    -
    2024年

    The 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)  Program Committee

  • 2023年
    -
    2024年

    The 17th International Symposium on Functional and Logic Programming (FLOPS 2024)  Program Committee

  • 2023年
    -
    2024年

    The 37th IEEE Computer Security Foundations Symposium (CSF 2024)  Program Committee

  • 2022年
    -
    2023年

    NII Shonan Meeting Seminar 180: The Art of SAT  Co-Organizer

  • 2022年
    -
    2023年

    The 21st Asian Symposium on Programming Languages and Systems (APLAS 2023)  SRC & Posters Selection Committee

  • 2022年
    -
    2023年

    The 21st International Symposium on Automated Technology for Verification and Analysis (ATVA 2023)  Program Committee

  • 2022年
    -
    2023年

    The 3rd International Conference on Code Quality (ICCQ 2023)  Program Committee

  • 2022年
    -
    2023年

    The 36th IEEE Computer Security Foundations Symposium (CSF 2023)  Program Committee

  • 2022年
    -
    2023年

    The 32nd European Symposium on Programming (ESOP 2023)  Program Committee

  • 2018年04月
    -
    2022年03月

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

  • 2021年
    -
    2022年

    The 37th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2022)  Program Committee

  • 2021年
    -
    2022年

    The 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022)  Program Committee

  • 2021年
    -
    2022年

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

  • 2021年
    -
    2022年

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

  • 2021年
    -
    2022年

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

  • 2020年
    -
    2021年

    Israel Science Foundation  Research Grant Application Reviewer

  • 2020年
    -
    2021年

    The International Conference on Software Testing, Machine Learning and Complex Process Analysis (TMPA-2021)  Program Committee

  • 2020年
    -
    2021年

    The 19th Asian Symposium on Programming Languages and Systems (APLAS 2021)  Program Committee

  • 2020年
    -
    2021年

    The 19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021)  Program Committee

  • 2020年
    -
    2021年

    The 33rd International Conference on Computer-Aided Verification (CAV 2021)  Program Committee

  • 2020年
    -
    2021年

    The 34th IEEE Computer Security Foundations Symposium (CSF 2021)  Program Committee

  • 2015年04月
    -
    2020年03月

    文部科学省 科学技術政策研究所 科学技術動向研究センター  専門調査員

  • 2019年
    -
    2020年

    The 15th International Symposium on Functional and Logic Programming (FLOPS 2020)  Program Committee

  • 2019年
    -
    2020年

    ソフトウェア科学会 第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020)  プログラム委員

  • 2019年
    -
    2020年

    The 12th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2020)  Program Committee

  • 2019年
    -
    2020年

    The 18th International Symposium on Automated Technology for Verification and Analysis (ATVA 2020)  Program Committee

  • 2018年
    -
    2019年

    The International Conference on Software Testing, Machine Learning and Complex Process Analysis (TMPA-2019)  Program Committee

  • 2018年
    -
    2019年

    The 26th International Symposium on Static Analysis (SAS 2019)  Program Committee

  • 2018年
    -
    2019年

    The 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)  Program Committee

  • 2018年
    -
    2019年

    The 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019)  Program Committee

  • 2018年
    -
    2019年

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

  • 2018年
    -
    2019年

    日本学術振興会  科学研究費委員会専門委員 (審査第三部会第60010小委員会 情報学基礎論関連)

  • 2014年04月
    -
    2018年03月

    情報処理学会プログラミング研究会(PRO)  運営委員

  • 2017年
    -
    2018年

    The 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018)  Program Committee

  • 2017年
    -
    2018年

    The 16th Asian Symposium on Programming Languages and Systems (APLAS 2018)  Program Committee

  • 2017年
    -
    2018年

    NII Shonan Seminar 115: Intensional and Extensional Aspects of Computation: From Computability and Complexity to Program Analysis and Security  Co-Organizer

  • 2017年
    -
    2018年

    The 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2018)  Program Committee

  • 2017年
    -
    2018年

    The 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018)  Program Committee

  • 2016年
    -
    2017年

    The 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017)  External Review Committee

  • 2016年
    -
    2017年

    The 26th European Symposium on Programming (ESOP 2017)  Program Committee

  • 2016年
    -
    2017年

    The 4th International Conference on Tools and Methods of Program Analysis (TMPA 2017)  Program Committee

  • 2016年
    -
    2017年

    The 11th International Workshop on Reachability Problems (RP 2017)  Program Committee

  • 2016年
    -
    2017年

    The 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)  Program Committee

  • 2016年
    -
    2017年

    The 15th Asian Symposium on Programming Languages and Systems (APLAS 2017)  Program Committee

  • 2015年
    -
    2016年

    The 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016) (Track B)  Program Committee

  • 2015年
    -
    2016年

    The 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016)  External Review Committee

  • 2015年
    -
    2016年

    The 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)  Program Committee

  • 2015年
    -
    2016年

    The 14th Asian Symposium on Programming Languages and Systems (APLAS 2016)  Program Committee

  • 2014年
    -
    2015年

    The 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015)  Program Committee

  • 2014年
    -
    2015年

    ACM SIGPLAN 10th Workshop on Programming Languages and Analysis for Security (PLAS 2015)  Program Committee

  • 2014年
    -
    2015年

    Workshop on Higher-Order Program Analysis (HOPA 2015)  Program Committee

  • 2014年
    -
    2015年

    NII Shonan Seminar 069: Logic and Verification Methods in Security and Privacy  Co-Organizer

  • 2013年
    -
    2014年

    電子情報通信学会 論文誌 第9回フォーマルアプローチ特集  編集委員

  • 2013年
    -
    2014年

    The 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014)  Program Committee

  • 2013年
    -
    2014年

    The 12th International Symposium on Functional and Logic Programming (FLOPS 2014)  Program Committee

  • 2013年
    -
    2014年

    Workshop on Higher-Order Program Analysis (HOPA 2014)  Program Committee

  • 2013年
    -
    2014年

    Joint Workshop on Foundations of Computer Security and Formal and Computational Cryptography (FCS-FCC'14)  Program Committee

  • 2012年
    -
    2013年

    電子情報通信学会 論文誌 第8回フォーマルアプローチ特集  編集委員

  • 2012年
    -
    2013年

    The 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013)  External Review Committee

  • 2012年
    -
    2013年

    The 22nd EACSL Annual Conference on Computer Science Logic (CSL 2013)  Program Committee

  • 2011年
    -
    2012年

    電子情報通信学会 論文誌 第7回フォーマルアプローチ特集  編集委員

  • 2011年
    -
    2012年

    The 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012)  Program Committee

  • 2011年
    -
    2012年

    The 10th Asian Symposium on Programming Languages and Systems (APLAS 2012)  Program Committee

  • 2010年
    -
    2011年

    The 6th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2011)  Program Committee

  • 2010年
    -
    2011年

    The 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2011)  Program Committee

  • 2010年
    -
    2011年

    The 5th ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV 2011)  Program Committee

  • 2010年
    -
    2011年

    The 20th European Symposium on Programming (ESOP 2011)  Program Committee

  • 2010年
    -
    2011年

    The 10th International Conference on Typed Lambda Calculi and Applications (TLCA 2011)  Program Committee

  • 2009年
    -
    2010年

    ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI 2010)  External Review Committee

  • 2009年
    -
    2010年

    ソフトウェア科学会 第12回プログラミングおよびプログラミング言語ワークショップ (PPL 2010)  プログラム共同委員長

  • 2009年
     
     

    ソフトウェア科学会 第11回プログラミングおよびプログラミング言語ワークショップ (PPL 2009)  プログラム委員

  • 2008年
    -
    2009年

    ACM SIGPLAN 4th Workshop on Programming Languages and Analysis for Security (PLAS 2009)  Program Committee

  • 2008年
    -
    2009年

    The 24th Annual ACM Symposium on Applied Computing (ACM SAC 2009) (Programming Languages Track)  Program Committee

  • 2007年
    -
    2008年

    The 15th International Static Analysis Symposium (SAS 2008)  Program Committee

▼全件表示

所属学協会

  •  
     
     

    ACM

  •  
     
     

    情報処理学会

  •  
     
     

    ソフトウェア科学会

研究分野

  • 情報セキュリティ / 情報学基礎論 / ソフトウェア

研究キーワード

  • プログラミング言語

  • 数理論理学

  • 形式検証

  • 形式言語理論

  • セキュリティ

  • プログラム検証

  • プログラム合成

  • 自動定理証明

  • 型システム

▼全件表示

受賞

  • 論文賞

    2024年03月   ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)   Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness  

    受賞者: 野上 大成, 寺内 多智弘

  • 論文賞

    2023年03月   ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)   後方参照付正規表現の表現力について  

    受賞者: 野上 大成, 寺内 多智弘

  • Distinguished Paper Award

    2023年01月   The 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)   Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification  

    受賞者: Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen

  • 辻井重男セキュリティ論文賞 大賞

    2022年10月   日本セキュリティ・マネジメント学会   Repairing DoS Vulnerability of Real-World Regexes  

    受賞者: 千田 忠賢, 寺内 多智弘

  • 論文賞

    2022年03月   ソフトウェア科学会 第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)   代数的エフェクトハンドラを持つ言語のためのトレースエフェクト  

    受賞者: 川俣 楓河, 寺内 多智弘

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

    2019年12月   早稲田大学  

    受賞者: 寺内 多智弘

  • Nominee, 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   Compositional Synthesis of Leakage Resilient Programs  

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

  • 第4回野口研究奨励賞

    2009年05月   情報処理学会 東北支部  

    受賞者: 寺内 多智弘

  • 発表賞(一般)

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

    受賞者: 寺内 多智弘

▼全件表示

 

論文

  • Repairing Regex-Dependent String Functions

    Nariyoshi Chida, Tachio Terauchi

    Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering     294 - 305  2024年10月  [査読有り]

    DOI

  • Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

    Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi

    Proceedings of the ACM on Programming Languages   8 ( POPL ) 115 - 147  2024年01月  [査読有り]  [国際誌]

     概要を見る

    Algebraic effects and handlers are a mechanism to structure programs with computational effects in a modular way. They are recently gaining popularity and being adopted in practical languages, such as OCaml. Meanwhile, there has been substantial progress in program verification via refinement type systems . While a variety of refinement type systems have been proposed, thus far there has not been a satisfactory refinement type system for algebraic effects and handlers. In this paper, we fill the void by proposing a novel refinement type system for languages with algebraic effects and handlers. The expressivity and usefulness of algebraic effects and handlers come from their ability to manipulate delimited continuations , but delimited continuations also complicate programs’ control flow and make their verification harder. To address the complexity, we introduce a novel concept that we call answer refinement modification (ARM for short), which allows the refinement type system to precisely track what effects occur and in what order when a program is executed, and reflect such information as modifications to the refinements in the types of delimited continuations. We formalize our type system that supports ARM (as well as answer type modification, or ATM) and prove its soundness. Additionally, as a proof of concept, we have extended the refinement type system to a subset of OCaml 5 which comes with a built-in support for effect handlers, implemented a type checking and inference algorithm for the extension, and evaluated it on a number of benchmark programs that use algebraic effects and handlers. The evaluation demonstrates that ARM is conceptually simple and practically useful. Finally, a natural alternative to directly reasoning about a program with delimited continuations is to apply a continuation passing style (CPS) transformation that transforms the program to a pure program without delimited continuations. We investigate this alternative in the paper, and show that the approach is indeed possible by proposing a novel CPS transformation for algebraic effects and handlers that enjoys bidirectional (refinement-)type-preservation. We show that there are pros and cons with this approach, namely, while one can use an existing refinement type checking and inference algorithm that can only (directly) handle pure programs, there are issues such as needing type annotations in source programs and making the inferred types less informative to a user.

    DOI

    Scopus

    3
    被引用数
    (Scopus)
  • On the Expressive Power of Regular Expressions with Backreferences

    Taisei Nogami, Tachio Terauchi

    In Proceedings of the 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), Leibniz International Proceedings in Informatics (LIPIcs) 272, pp.71:1-71:15, Schloss Dagstuhl Leibniz-Zentrum für Informatik    2023年08月  [査読有り]  [国際誌]

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト

    川俣 楓河, 寺内 多智弘

    コンピュータソフトウェア   40 ( 2 ) 2_19 - 2_48  2023年06月  [査読有り]  [招待有り]  [国内誌]

    DOI

    Scopus

  • Repairing Regular Expressions for Extraction

    Nariyoshi Chida, Tachio Terauchi

    Proceedings of the ACM on Programming Languages   7 ( PLDI ) 1633 - 1656  2023年06月  [査読有り]  [国際誌]

     概要を見る

    While synthesizing and repairing regular expressions (regexes) based on Programming-by-Examples (PBE) methods have seen rapid progress in recent years, all existing works only support synthesizing or repairing regexes for membership testing, and the support for extraction is still an open problem. This paper fills the void by proposing the first PBE-based method for synthesizing and repairing regexes for extraction. Our work supports regexes that have real-world extensions such as backreferences and lookarounds. The extensions significantly affect the PBE-based synthesis and repair problem. In fact, we show that there are unsolvable instances of the problem if the synthesized regexes are not allowed to use the extensions, i.e., there is no regex without the extensions that correctly classify the given set of examples, whereas every problem instance is solvable if the extensions are allowed. This is in stark contrast to the case for the membership where every instance is guaranteed to have a solution expressible by a pure regex without the extensions. The main contribution of the paper is an algorithm to solve the PBE-based synthesis and repair problem for extraction. Our algorithm builds on existing methods for synthesizing and repairing regexes for membership testing, i.e., the enumerative search algorithms with SMT constraint solving. However, significant extensions are needed because the SMT constraints in the previous works are based on a non-deterministic semantics of regexes. Non-deterministic semantics is sound for membership but not for extraction, because which substrings are extracted depends on the deterministic behavior of actual regex engines. To address the issue, we propose a new SMT constraint generation method that respects the deterministic behavior of regex engines. For this, we first define a novel formal semantics of an actual regex engine as a deterministic big-step operational semantics, and use it as a basis to design the new SMT constraint generation method. The key idea to simulate the determinism in the formal semantics and the constraints is to consider continuations of regex matching and use them for disambiguation. We also propose two new search space pruning techniques called approximation-by-pure-regex and approximation-by-backreferences that make use of the extraction information in the examples. We have implemented the synthesis and repair algorithm in a tool called R3 (Repairing Regex for extRaction) and evaluated it on 50 regexes that contain real-world extensions. Our evaluation shows the effectiveness of the algorithm and that our new pruning techniques substantially prune the search space.

    DOI

    Scopus

    5
    被引用数
    (Scopus)
  • On Lookaheads in Regular Expressions with Backreferences

    Nariyoshi Chida, Tachio Terauchi

    IEICE Transactions on Information and Systems   E106.D ( 5 ) 959 - 975  2023年05月  [査読有り]  [国内誌]

    DOI

  • Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

    Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen

    Proceedings of the ACM on Programming Languages   7 ( POPL ) 2111 - 2140  2023年01月  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We present a novel approach to deciding the validity of formulas in first-order fixpoint logic with background theories and arbitrarily nested inductive and co-inductive predicates defining least and greatest fixpoints. Our approach is constraint-based, and reduces the validity checking problem of the given first-order-fixpoint logic formula (formally, an instance in a language called µCLP) to a constraint satisfaction problem for a recently introduced predicate constraint language.

    Coupled with an existing sound-and-relatively-complete solver for the constraint language, this novel reduction alone already gives a sound and relatively complete method for deciding µCLP validity, but we further improve it to a novel modular primal-dual method. The key observations are (1) µCLP is closed under complement such that each (co-)inductive predicate in the original primal instance has a corresponding (co-)inductive predicate representing its complement in the dual instance obtained by taking the standard De Morgan’s dual of the primal instance, and (2) partial solutions for (co-)inductive predicates synthesized during the constraint solving process of the primal side can be used as sound upper-bounds of the corresponding (co-)inductive predicates in the dual side, and vice versa. By solving the primal and dual problems in parallel and exchanging each others’ partial solutions as sound bounds, the two processes mutually reduce each others’ solution spaces, thus enabling rapid convergence. The approach is also modular in that the bounds are synthesized and exchanged at granularity of individual (co-)inductive predicates.

    We demonstrate the utility of our novel fixpoint logic solving by encoding a wide variety of temporal verification problems in µCLP, including termination/non-termination, LTL, CTL, and even the full modal µ-calculus model checking of infinite state programs. The encodings exploit the modularity in both the program and the property by expressing each loops and (recursive) functions in the program and sub-formulas of the property as individual (possibly nested) (co-)inductive predicates. Together with our novel modular primal-dual µCLP solving, we obtain a novel approach to efficiently solving a wide range of temporal verification problems.

    DOI

    Scopus

    3
    被引用数
    (Scopus)
  • On Lookaheads in Regular Expressions with Backreferences

    Nariyoshi Chida, Tachio Terauchi

    In Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), Leibniz International Proceedings in Informatics (LIPIcs) 228, pp.15:1-15:18, Schloss Dagstuhl Leibniz-Zentrum für Informatik    2022年08月  [査読有り]  [国際誌]

    DOI

    Scopus

    6
    被引用数
    (Scopus)
  • Repairing DoS Vulnerability of Real-World Regexes

    Nariyoshi Chida, Tachio Terauchi

    In Proceedings of the 43rd IEEE Symposium on Security and Privacy (S&P 2022), pp.2060-2077, IEEE Computer Society    2022年05月  [査読有り]  [国際誌]

    DOI

    Scopus

    6
    被引用数
    (Scopus)
  • Constraint-based Relational Verification

    Hiroshi Unno, Tachio Terauchi, Eric Koskinen

    In Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021), Lecture Notes in Computer Science 12759, pp.742-766, Springer    2021年  [査読有り]  [国際誌]  [国際共著]

    DOI

    Scopus

    25
    被引用数
    (Scopus)
  • Bucketing and Information Flow Analysis for Provable Timing Attack Mitigation

    Tachio Terauchi, Timos Antonopoulos

    Journal of Computer Security   28 ( 6 ) 607 - 634  2020年  [査読有り]  [国際誌]  [国際共著]

    DOI

    Scopus

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

    Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

    コンピュータソフトウェア   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

    Scopus

    6
    被引用数
    (Scopus)
  • Games for Security under Adaptive Adversaries.

    Timos Antonopoulos, Tachio Terauchi

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

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • 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), Lecture Notes in Computer Science 11426, pp.29-50, Springer    2019年  [査読有り]  [国際誌]  [国際共著]

    DOI

    Scopus

    3
    被引用数
    (Scopus)
  • 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), pp. 759-768, ACM    2018年  [査読有り]  [国際誌]  [国際共著]

    DOI

    Scopus

    16
    被引用数
    (Scopus)
  • Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs.

    Hiroshi Unno, Yuki Satake, Tachio Terauchi

    Proceedings of the ACM on Programming Languages   2 ( POPL ) 12:1-12:29  2018年  [査読有り]  [国際誌]

    DOI

    Scopus

    12
    被引用数
    (Scopus)
  • Compositional Synthesis of Leakage Resilient Programs

    Arthur Blot, Masaki Yamamoto, Tachio Terauchi

    In Proceedings of the 6th International Conference on Principles of Security and Trust (POST 2017), Lecture Notes in Computer Science 10204, pp.277-297, Springer    2017年  [査読有り]  [国際誌]

     概要を見る

    A promising approach to defend against side channel attacks is to build programs that are leakage resilient, in a formal sense. One such formal notion of leakage resilience is the n-threshold-probing model proposed in the seminal work by Ishai et al. [16]. In a recent work [9], Eldib and Wang have proposed a method for automatically synthesizing programs that are leakage resilient according to this model, for the case n = 1. In this paper, we show that the n-threshold-probing model of leakage resilience enjoys a certain compositionality property that can be exploited for synthesis.We use the property to design a synthesis method that efficiently synthesizes leakage-resilient programs in a compositional manner, for the general case of n &gt
    1. We have implemented a prototype of the synthesis algorithm, and we demonstrate its effectiveness by synthesizing leakage-resilient versions of benchmarks taken from the literature.

    DOI

    Scopus

    11
    被引用数
    (Scopus)
  • Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels

    Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, Shiyi Wei

    In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), ACM SIGPLAN Notices 52 (6), pp.362-375. ACM    2017年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We present a novel approach to proving the absence of timing channels. The idea is to partition the program's execution traces in such a way that each partition component is checked for timing attack resilience by a time complexity analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by splitting the program traces at secret-independent branches. This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, the per-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus in contrast to prior approaches, such as self-composition, that aim to reason about multiple (k &gt;= 2) executions at once.
    We formalize the above as an approach called quotient partitioning, generalized to any k-safety property, and prove it to be sound. A key feature of our approach is a demand-driven partitioning strategy that uses a regex-like notion called trails to identify sets of execution traces, particularly those influenced by tainted (or secret) data. We have applied our technique in a prototype implementation tool called Blazer, based on WALA, PPL, and the brics automaton library. We have proved timing-channel freedom of (or synthesized an attack specification for) 24 programs written in Java bytecode, including 6 classic examples from the literature and 6 examples extracted from the DARPA STAC challenge problems.

    DOI

    Scopus

    20
    被引用数
    (Scopus)
  • Temporal Verification of Higher-order Functional Programs

    Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

    In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices 51 (1), pp.57-68, ACM.    2016年  [査読有り]  [国際誌]

     概要を見る

    We present an automated approach to verifying arbitrary omega regular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the "calling relation" is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.

    DOI

    Scopus

    9
    被引用数
    (Scopus)
  • Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling

    Hiroshi Unno, Tachio Terauchi

    In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), Lecture Notes in Computer Science 9035, pp.149-163, Springer    2015年  [査読有り]  [国際誌]

     概要を見る

    Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.

    DOI

    Scopus

    7
    被引用数
    (Scopus)
  • Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR

    Tachio Terauchi

    In Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Lecture Notes in Computer Science 9291, pp.128-144, Springer    2015年  [査読有り]  [国際誌]

     概要を見る

    Safety property (i.e., reachability) verification is undecidable for Turing-complete programming languages. Nonetheless, recent progress has lead to heuristic verification methods, such as the ones based on predicate abstraction with counter example-guided refinement (CEGAR), that work surprisingly well in practice. In this paper, we investigate the effectiveness of the small refinement heuristic which, for abstraction refinement in CEGAR, uses (the predicates in) a small proof of the given counterexample's spuriousness [3,12,17,22]. Such a method has shown to be quite effective in practice but thus far lacked a theoretical backing. Our core result is that the heuristic guarantees certain bounds on the number of CEGAR iterations, relative to the size of a proof for the input program.

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement

    Tachio Terauchi, Hiroshi Unno

    In Proceedings of the 24th European Symposium on Programming (ESOP 2015), Lecture Notes in Computer Science 9032, pp.610-633, Springer    2015年  [査読有り]  [国際誌]

     概要を見る

    In counterexample-guided abstraction refinement, a predicate refinement scheme is said to be complete for a given theory if it is guaranteed to eventually find predicates sufficient to prove the given property, when such exist. However, existing complete methods require deciding if a proof of the counterexample's spuriousness exists in some finite language of predicates. Such an exact finite-language-restricted predicate search is quite hard for many theories used in practice and incurs a heavy overhead. In this paper, we address the issue by showing that the language restriction can be relaxed so that the refinement process is restricted to infer proofs from some finite language L-base boolean OR L-ext but is only required to return a proof when the counterexample's spuriousness can be proved in L-base. Then, we show how a proof-based refinement algorithm can be made to satisfy the relaxed requirement and be complete by restricting only the theory-level reasoning in SMT to emit L-base-restricted partial interpolants (while such an approach has been proposed previously, we show for the first time that it can be done for languages that are not closed under conjunctions and disjunctions). We also present a technique that uses a property of counterexample patterns to further improve the efficiency of the refinement algorithm while still satisfying the requirement. We have experimented with a prototype implementation of the new refinement algorithm, and show that it is able to achieve complete refinement with only a small overhead.

    DOI

    Scopus

    3
    被引用数
    (Scopus)
  • Automatic Termination Verification for Higher-Order Functional Programs

    Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi

    In Proceedings of the 23rd European Symposium on Programming (ESOP 2014), Lecture Notes in Computer Science 8410, pp.392-411, Springer    2014年  [査読有り]  [国際誌]

     概要を見る

    We present an automated approach to verifying termination of higher-order functional programs. Our approach adopts the idea from the recent work on termination verification via transition invariants (a.k.a. binary reachability analysis), and is fully automated. Our approach is able to soundly handle the subtle aspects of higher-order programs, including partial applications, indirect calls, and ranking functions over function closure values. In contrast to the previous approaches to automated termination verification for functional programs, our approach is sound and complete, relative to the soundness and completeness of the underlying reachability analysis and ranking function inference. We have implemented a prototype of our approach for a subset of the OCaml language, and we have confirmed that it is able to automatically verify termination of some non-trivial higher-order programs.

    DOI

    Scopus

    30
    被引用数
    (Scopus)
  • Local Temporal Reasoning

    Eric Koskinen, Tachio Terauchi

    In Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014), pp.59:1-59:10, ACM    2014年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We present the first method for reasoning about temporal logic properties of higher-order, infinite-data programs. By distinguishing between the finite traces and infinite traces in the specification, we obtain rules that permit us to reason about the temporal behavior of program parts via a type-and-effect system, which is then able to compose these facts together to prove the overall target property of the program. The type system alone is strong enough to derive many temporal safety properties using refinement types and temporal effects. We also show how existing techniques can be used as oracles to provide liveness information (e.g. termination) about program parts and that the type-and-effect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higher-order software, as well as modular strategies for procedural programs. Copyright © 2014 ACM.

    DOI

    Scopus

    24
    被引用数
    (Scopus)
  • Quantitative Information Flow as Safety and Liveness Hyperproperties

    Hirotoshi Yasuoka, Tachio Terauchi

    Theoretical Computer Science   538   167 - 182  2014年  [査読有り]  [招待有り]  [国際誌]

     概要を見る

    We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call "k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition. (C) 2013 Elsevier B.V. All rights reserved.

    DOI

    Scopus

    18
    被引用数
    (Scopus)
  • Automating Relatively Complete Verification of Higher-order Functional Programs

    Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

    In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), ACM SIGPLAN Notices 48 (1), pp.75-86, ACM, January, 2013.    2013年01月  [査読有り]  [国際誌]

     概要を見る

    We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work on (incomplete) automated higher-order verification by drawing on the classical work on relatively complete "Hoare logic like" program logic for higher-order procedural languages. Then, by adopting the recently proposed techniques for solving constraints over quantified first-order logic formulas, we develop an automated type inference method for the type system, thereby realizing an automated relatively complete verification of higher-order programs. Copyright © 2013 ACM.

    DOI

    Scopus

    12
    被引用数
    (Scopus)
  • 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて

    岩塚 卓弥, 寺内 多智弘, 結縁 祥治

    情報処理学会論文誌プログラミング(PRO)   6 ( 3 ) 20 - 32  2013年  [査読有り]  [国内誌]

    CiNii

  • Quantitative Information Flow as Safety and Liveness Hyperproperties

    Hirotoshi Yasuoka, Tachio Terauchi

    In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), Electronic Proceedings in Theoretical Computer Science 85, pp.77-91    2012年  [査読有り]  [国際誌]

     概要を見る

    We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call "k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition.

    DOI

    Scopus

    4
    被引用数
    (Scopus)
  • On Bounding Problems of Quantitative Information Flow

    Hirotoshi Yasuoka, Tachio Terauchi

    Journal of Computer Security   19 ( 6 ) 1029 - 1082  2011年  [査読有り]  [招待有り]  [国際誌]

     概要を見る

    Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, belief, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the "bounding problem" of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free Boolean programs. Specifically, we show that the problem is PP-hard for all definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow. © 2011 - IOS Press and the authors. All rights reserved.

    DOI

    Scopus

    15
    被引用数
    (Scopus)
  • Dependent Types from Counterexamples

    Tachio Terauchi

    In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), ACM SIGPLAN Notices 45 (1), pp.119-130, ACM    2010年  [査読有り]  [国際誌]

     概要を見る

    Motivated by recent research in abstract model checking, we present a new approach to inferring dependent types. Unlike many of the existing approaches, our approach does not rely on programmers to supply the candidate (or the correct) types for the recursive functions and instead does counterexample-guided refinement to automatically generate the set of candidate dependent types. The main idea is to extend the classical fixed-point type inference routine to return a counterexample if the program is found untypable with the current set of candidate types. Then, an interpolating theorem prover is used to validate the counterexample as a real type error or generate additional candidate dependent types to refute the spurious counterexample. The process is repeated until either a real type error is found or sufficient candidates are generated to prove the program typable. Our system makes non-trivial use of "linear" intersection types in the refinement phase.
    The paper presents the type inference system and reports on the experience with a prototype implementation that infers dependent types for a subset of the Ocaml language. The implementation infers dependent types containing predicates from the quantifier-free theory of linear arithmetic and equality with uninterpreted function symbols.

    DOI

    Scopus

    14
    被引用数
    (Scopus)
  • On Bounding Problems of Quantitative Information Flow

    Hirotoshi Yasuoka, Tachio Terauchi

    In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS 2010), Lecture Notes in Computer Science 6345, pp.357-372, Springer    2010年  [査読有り]  [国際誌]

     概要を見る

    Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the "bounding problem" of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not; a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not; amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free boolean programs. Specifically, we show that the problem is PP-hard for all the definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow.

    DOI

    Scopus

    14
    被引用数
    (Scopus)
  • Quantitative Information Flow - Verification Hardness and Possibilities

    Hirotoshi Yasuoka, Tachio Terauchi

    In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), pp.15-27, IEEE Computer Society    2010年  [査読有り]  [国際誌]

     概要を見る

    Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, and channel capacity. This paper investigates the hardness and possibilities of precisely checking and inferring quantitative information flow according to such definitions.
    We prove that, even for just comparing two programs on which has the larger flow, none of the definitions is a k-safety property for any k, and therefore is not amenable to the self-composition technique that has been successfully applied to precisely checking non-interference. We also show a complexity theoretic gap with non-interference by proving that, for loop-free boolean programs whose non-interference is coNP-complete, the comparison problem is #P-hard for all of the definitions.
    For positive results, we show that universally quantifying the distribution in the comparison problem, that is, comparing two programs according to the entropy based definitions on which has the larger flow for all distributions, is a 2-safety problem in general and is coNP-complete when restricted for loop-free boolean programs. We prove this by showing that the problem is equivalent to a simple relation naturally expressing the fact that one program is more secure than the other. We prove that the relation also refines the channel-capacity based definition, and that it can be precisely checked via the self-composition as well as the "interleaved" self-composition technique.

    DOI

    Scopus

    44
    被引用数
    (Scopus)
  • Polymorphic Fractional Capabilities

    Hirotoshi Yasuoka, Tachio Terauchi

    In Proceedings of the 16th International Static Analysis Symposium (SAS 2009), Lecture Notes in Computer Science 5673, pp.36-51, Springer.    2009年  [査読有り]  [国際誌]

     概要を見る

    The capability calculus is a framework for statically reasoning about program resources such as deallocatable memory regions. Fractional capabilities, originally proposed by Boyland for checking the determinism of parallel reads hi multi-thread programs, extend the capability calculus by extending the capabilities to range over the rational numbers. Fractional capabilities have since found numerous applications, including race detection, buffer bound inference, security analyses, and separation logic. However, previous work on fractional capability systems either lacked polymorphism or lacked an efficient inference procedure. Automated inference is important; for the application of the calculus to static analysis. This paper addresses the issue by presenting a, polymorphic fractional capability calculus that, allows polynomial-time inference via a reduction to rational linear programming.

    DOI

    Scopus

    5
    被引用数
    (Scopus)
  • Witnessing Side Effects

    Tachio Terauchi, Alex Aiken

    ACM Transactions on Programming Languages and Systems (TOPLAS)   30 ( 3 ) 15:1-15:42  2008年05月  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We present a new approach to the old problem of adding global mutable state to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a somewhat surprising static checking algorithm that makes use of a network flow property equivalent to the semantic condition via reduction to a satisfaction problem for a system of linear inequalities.

    DOI

    Scopus

    6
    被引用数
    (Scopus)
  • A Capability Calculus for Concurrency and Determinism

    Tachio Terauchi, Alex Aiken

    ACM Transactions on Programming Languages and Systems (TOPLAS)   30 ( 5 ) 27:1 - 27:30  2008年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    This article presents a static system for checking determinism (technically, partial confluence) of communicating concurrent processes. Our approach automatically detects partial confluence in programs communicating via a mix of different kinds of communication methods: rendezvous channels, buffered channels, broadcast channels, and reference cells. Our system reduces the partial confluence checking problem in polynomial time (in the size of the program) to the problem of solving a system of rational linear inequalities, and is thus efficient.

    DOI

    Scopus

    22
    被引用数
    (Scopus)
  • Checking Race Freedom via Linear Programming

    Tachio Terauchi

    In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008), ACM SIGPLAN Notices 43 (6), pp.1-10, ACM    2008年  [査読有り]  [国際誌]

     概要を見る

    We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to ( rational) linear programming. Unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. We achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying an implementation to real world C programs.

    DOI

    Scopus

    6
    被引用数
    (Scopus)
  • Inferring Channel Buffer Bounds via Linear Programming

    Tachio Terauchi, Adam Megacz

    In Proceedings of the 17th European Symposium on Programming (ESOP 2008), Lecture Notes in Computer Science 4960, pp.284-298, Springer    2008年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We present a static analysis for inferring the maximum amount of buffer space used by a program consisting of concurrently running processes communicating via buffered channels. We reduce the problem to linear programming by casting the analysis as a fractional capability calculus system. Our analysis can reason about buffers used by multiple processes concurrently, and runs in time polynomial in the size of the program.

    DOI

    Scopus

    2
    被引用数
    (Scopus)
  • A Type System for Observational Determinism

    Tachio Terauchi

    In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp.287-300, IEEE Computer Society    2008年  [査読有り]  [国際誌]

     概要を見る

    Zdancewic and Myers introduced observational determinism as a scheduler independent notion of security for concurrent programs. This paper proposes a type system for verifying observational determinism. Our type system verifies observational determinism by itself and does not require the type checked program to be confluent. A polynomial time type inference algorithm is also presented.

    DOI

    Scopus

    32
    被引用数
    (Scopus)
  • On Typability for Rank-2 Intersection Types with Polymorphic Recursion

    Tachio Terauchi, Alex Aiken

    In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS 2006), pp.111-122, IEEE Computer Society    2006年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We show that typability for a natural form of polymorphic recursive typing for rank-2 intersection types is undecidable. Our proof involves characterizing typability as a conte-xtfree language (CFL) graph problem, which may be of independent interest, and reduction from the boundedness problemfor Turing machines. We also show a property of the type system which, in conjunction with the undecidability result, disproves a misconception about the MilnerMycroft type system. We also show undecidability of a related program analysis problem.

    DOI

    Scopus

    3
    被引用数
    (Scopus)
  • A Capability Calculus for Concurrency and Determinism

    Tachio Terauchi, Alex Aiken

    In Proceedings of the 17th International Conference on Concurrency Theory (CONCUR 2006), Lecture Notes in Computer Science 4137, pp.218-232, Springer    2006年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We present a capability calculus for checking partial confluence of channel-communicating concurrent processes. Our approach automatically detects more programs to be partially confluent than previous approaches and is able to handle a mix of different kinds of communication channels, including shared reference cells.

    DOI

    Scopus

    11
    被引用数
    (Scopus)
  • Secure Information Flow as a Safety Problem

    Tachio Terauchi, Alexander Aiken

    In Proceedings of the 12th International Static Analysis Symposium (SAS 2005), Lecture Notes in Computer Science 3672, pp.352-367, Springer, September, 2005.    2005年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    The termination insensitive secure information flow problem can be reduced to solving a safety problem via a simple program transformation. Barthe, D'Argenio, and Rezk coined the term "self-composition" to describe this reduction. This paper generalizes the self-compositional approach with a form of information downgrading recently proposed by Li and Zdancewic. We also identify a problem with applying the self-compositional approach in practice, and we present a solution to this problem that makes use of more traditional type-based approaches. The result is a framework that combines the best of both worlds, i.e., better than traditional type-based approaches and better than the self-compositional approach.

    DOI

    Scopus

    195
    被引用数
    (Scopus)
  • Witnessing Side-Effects

    Tachio Terauchi, Alex Aiken

    In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), ACM SIGPLAN Notices 40 (9), pp.105-115, ACM    2005年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We present a new approach to the old problem of adding side effects to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a static checking algorithm that makes use of a network flow property equivalent to the semantic condition.

    DOI

    Scopus

    7
    被引用数
    (Scopus)
  • Checking and Inferring Local Non-Aliasing

    Alex Aiken, Jeffrey S. Foster, John Kodumal, Tachio Terauchi

    In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), ACM SIGPLAN Notices 38 (5), pp.129-140, ACM    2003年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    In prior work [15] we studied a language construct restrict that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other applications, programming with these constructs helps program analysis tools locally recover strong updates, which can improve the tracking of state in flow-sensitive analyses. In this paper we continue the study of restrict and introduce the construct confine. We present a type and effect system for checking the correctness of these annotations, and we develop efficient constraint-based algorithms implementing these type checking systems. To make it easier to use restrict and confine in practice, we show how to automatically infer such annotations without programmer assistance. In experiments on locking in 589 Linux device drivers, confine inference can automatically recover strong updates to eliminate 95% of the type errors resulting from weak updates.

    DOI

  • Flow-Sensitive Type Qualifiers

    Jeffrey S. Foster, Tachio Terauchi, Alex Aiken

    In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), ACM SIGPLAN Notices 37 (5), pp.1-12, ACM    2002年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type, qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled flow-sensitively-the underlying standard types are unchanged, which allows us to obtain an efficient constraint-based inference algorithm that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates. We demonstrate the usefulness of flow-sensitive type qualifiers by finding a number of new locking bugs in the Linux kernel.

    DOI

  • Exploring MARS: Developing Indoor and Outdoor User Interfaces to a Mobile Augmented Reality System

    Tobias Hollerer, Steven Feiner, Tachio Terauchi, Gus Rashid, Drexel Hallaway

    Computers & Graphics   23 ( 6 ) 779 - 785  1999年  [査読有り]  [国際誌]  [国際共著]

     概要を見る

    We describe an experimental mobile augmented reality system (MARS) testbed that employs different user interfaces to allow outdoor and indoor users to access and manage information that is spatially registered with the real world. Outdoor users can experience spatialized multimedia presentations that are presented on a head-tracked, see-through, head-worn display used in conjunction with a hand-held pen-based computer. Indoor users can get an overview of the outdoor scene and communicate with outdoor users through a desktop user interface or a head- and hand-tracked immersive augmented reality user interface. (C) 1999 Elsevier Science Limited. All rights reserved.

    DOI

    Scopus

    319
    被引用数
    (Scopus)

▼全件表示

講演・口頭発表等

  • Repairing DoS Vulnerability of Real-World Regexes

    Tachio Terauchi  [招待有り]

    NII Shonan Meeting Seminar 159: Web Application Security  

    発表年月: 2024年03月

  • Repairing Regular Expressions for Extraction

    Nariyoshi Chida, Tachio Terauchi

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

    発表年月: 2024年03月

  • Nested Data Type における多相再帰のための主要型付けを持つ型システム

    川原 知真, 寺内 多智弘

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

    発表年月: 2024年03月

  • Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

    Fuga Kawamata, Taro Sekiyama, Hiroshi Unno, Tachio Terauchi

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

    発表年月: 2024年03月

  • Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness

    野上 大成, 寺内 多智弘

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

    発表年月: 2024年03月

  • Repairing DoS Vulnerability of Real-World Regexes

    Tachio Terauchi  [招待有り]

    Technology Challenges in Non-Traditional Security  

    発表年月: 2023年10月

  • Applications of Program Verification and Synthesis Techniques to Security, from Non-Interference to ReDoS

    Tachio Terauchi  [招待有り]

    Vietnam-Japan Autumn School on Cyber Security  

    発表年月: 2023年10月

  • Repairing DoS Vulnerability of Real-World Regexes

    Tachio Terauchi

    NII Shonan Meeting Seminar 180:The Art of SAT  

    発表年月: 2023年10月

  • Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

    Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi  [招待有り]

    NII Shonan Meeting Seminar 203:Effect Handlers and General-Purpose Languages  

    発表年月: 2023年10月

  • Repairing DoS Vulnerability of Real-World Regexes

    Nariyoshi Chida, Tachio Terauchi  [招待有り]

    第22回情報科学技術フォーラム(FIT2023)  

    発表年月: 2023年09月

  • On Lookaheads in Regular Expressions with Backreferences

    Nariyoshi Chida, Tachio Terauchi

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

    発表年月: 2023年03月

  • On Lookaheads in Regular Expressions with Backreferences (Poster Presentation)

    Nariyoshi Chida, Tachio Terauchi

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

    発表年月: 2023年03月

  • Nested Data Type における多相再帰の型推論手法 (ポスター発表)

    川原 知真, 寺内 多智弘

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

    発表年月: 2023年03月

  • 代数的エフェクトハンドラのための篩型システム (ポスター発表)

    川俣 楓河, 海野 広志, 関山 太郎, 寺内 多智弘

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

    発表年月: 2023年03月

  • Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

    Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen

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

    発表年月: 2023年03月

  • 後方参照付正規表現の表現力について

    野上 大成, 寺内 多智弘

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

    発表年月: 2023年03月

  • Repairing DoS Vulnerability of Real-World Regexes (from IEEE S&P 2022)

    Nariyoshi Chida, Tachio Terauchi  [招待有り]

    2022年 暗号と情報セキュリティワークショップ  

    発表年月: 2022年09月

  • Repairing DoS Vulnerability of Real-World Regexes

    Nariyoshi Chida, Tachio Terauchi

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

    発表年月: 2022年03月

  • 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト

    川俣 楓河, 寺内 多智弘

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

    発表年月: 2022年03月

  • Constraint-based Relational Verification

    Tachio Terauchi  [招待有り]

    Workshop on Hyperproperties: Advances in Theory and Practice (HYPER 2021)  

    発表年月: 2021年10月

  • 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

    Tachio Terauchi  [招待有り]

    Dagstuhl Seminar 19371: Deduction Beyond Satisfiability  

    発表年月: 2019年09月

  • Solving First-Order Fixpoint Logic for Program Verification

    Tachio Terauchi  [招待有り]

    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月

  • A Fixpoint Logic and Dependent Effects for Temporal Property Verification

    Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

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

    発表年月: 2019年03月

  • On Cut-elimination in Cyclic Proof Systems

    Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

    The 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)  

    発表年月: 2018年12月

  • Information Flow Security and its Applications to Side Channel Attack Resilience

    Tachio Terauchi  [招待有り]

    The 4th Franco-Japanese Workshop on Cybersecurity  

    発表年月: 2018年05月

  • Dependent Temporal Effects and Fixpoint Logic for Verification (Poster Presentation)

    Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

    ソフトウェア科学会 第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018)  

    発表年月: 2018年03月

  • Compositional Synthesis of Leakage Resilient Programs.

    Tachio Terauchi

    NII Shonan Meeting Seminar 115: Intensional and Extensional Aspects of Computation: From Computability and Complexity to Program Analysis and Security  

    発表年月: 2018年01月

  • On Predicate Refinement Heuristics in Program Verification with CEGAR

    Tachio Terauchi  [招待有り]

    The 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016)  

    発表年月: 2016年04月

  • On Temporal Verification of Higher-Order Functional Programs

    Tachio Terauchi  [招待有り]

    NII Shonan Meeting Seminar 078: Higher-Order Model Checking  

    発表年月: 2016年03月

  • Temporal Verification of Higher-Order Functional Programs

    Tachio Terauchi  [招待有り]

    Dagstuhl Seminar 16131: Language Based Verification Tools for Functional Programs  

    発表年月: 2016年03月

  • Verification of Object-Oriented Programs via Refinement Types (Poster presentation)

    Nam Mai, Tachio Terauchi

    The 13th Asian Symposium on Programming Languages and Systems (APLAS 2015)  

    発表年月: 2015年11月

  • Predicate Refinement Heuristics in Program Verification with CEGAR

    Tachio Terauchi  [招待有り]

    NII Shonan Meeting Seminar 063: Semantics and Verification of Object-Oriented Languages  

    発表年月: 2015年09月

  • Information Flow Analysis and Applications to Computer Security

    Tachio Terauchi  [招待有り]

    NII Shonan Meeting Seminar 065: Low-level Code Analysis and Applications to Computer Security  

    発表年月: 2015年03月

  • 効率の良いLeakage Resilientプログラムの自動生成に向けて (ポスター発表)

    山本 真輝, 寺内 多智弘

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

    発表年月: 2015年03月

  • プログラム検証とインバリアント生成

    寺内 多智弘  [招待有り]

    ソフトウェア科学会第31回全国大会  

    発表年月: 2014年09月

  • On Complexity of Verifying Quantitative Information Flow

    Tachio Terauchi  [招待有り]

    Dagstuhl Seminar 12481: Quantitative Security Analysis  

    発表年月: 2012年11月

  • Automated Verification of Higher-Order Functional Programs

    Tachio Terauchi  [招待有り]

    The 11th International Symposium on Functional and Logic Programming (FLOPS 2012)  

    発表年月: 2012年05月

  • Relatively Complete Refinement Types from Counterexamples

    Tachio Terauchi  [招待有り]

    NII Shonan Meeting Seminar 005: Automated Techniques for Higher-Order Program Verification  

    発表年月: 2011年09月

  • Polymorphic Fractional Capabilities

    Hirotoshi Yasuoka, Tachio Terauchi

    ソフトウェア科学会 第12回 プログラミングおよびプログラミング言語ワークショップ (PPL 2010),  

    発表年月: 2010年03月

  • 量的情報流の検証の困難性と可能性について. (ポスター発表)

    安岡 宏俊, 寺内 多智弘

    ソフトウェア科学会 第12回 プログラミングおよびプログラミング言語ワークショップ (PPL 2010),  

    発表年月: 2010年03月

  • Dependent Types from Counterexamples (ポスター発表)

    寺内 多智弘

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

    発表年月: 2010年03月

  • Checking Race Freedom via Linear Programming.

    寺内 多智弘

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

    発表年月: 2008年03月

  • Classification of Cancer Tissue Types by Support Vector Machines using Micro Array Gene Expression Data (Poster presentation)

    Jinsong Cai, Aynur Dayanik, Hong Yu, Naveed Hasan, Tachio Terauchi, William N. Grundy

    The 8th International Conference on Intelligent Systems for Molecular Biology (ISMB 2000)  

    発表年月: 2000年08月

▼全件表示

共同研究・競争的資金等の研究課題

  • 依存篩型と述語制約によるプログラム検証の深化

    日本学術振興会  科学研究費助成事業 基盤研究(B)

    研究期間:

    2022年04月
    -
    2027年03月
     

    寺内 多智弘, 海野 広志

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

    日本学術振興会  科学研究費助成事業 挑戦的研究(開拓)

    研究期間:

    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月
     

    石原 哉

  • 論理的ー形式的手法による情報セキュリティ研究ー暗号プロトコル検証と量的情報流解析

    日本学術振興会  二国間交流事業 共同研究 (AYAMEプログラム)

    研究期間:

    2016年04月
    -
    2019年03月
     

    岡田 光弘

  • 実用効率の振舞いに基づくソフトウェア検証の数理的構造

    日本学術振興会  二国間交流事業 共同研究

    研究期間:

    2015年04月
    -
    2017年12月
     

    結縁 祥治

  • 高階プログラミング言語で記述された大規模ソフトウェアの検証

    日本学術振興会  科学研究費助成事業 基盤研究(C)

    研究期間:

    2014年04月
    -
    2017年03月
     

    寺内 多智弘

     概要を見る

    本課題の目標は、関数型プログラミング言語など、高階関数を含むプログラミング言語で記述された大規模ソフトウェアに対して有効な自動検証手法の確立である。特に、近年、国内外において高く注目されている依存型型システムを用いたソフトウェアモデル検査による手法を研究した。
    <BR>
    主な研究成果は以下である:1.)よりよい抽象詳細化(ソフトウェアモデル検査に用いられる技術)の手法、2.)高階関数型プログラムのための停止性・活性仕様など時相論理仕様の自動検証手法。

  • 高レベル言語で記述されたリアクティブシステムに対する実時間性質の検証

    日本学術振興会  科学研究費助成事業 基盤研究(B)

    研究期間:

    2013年04月
    -
    2017年03月
     

    結縁 祥治, 寺内 多智弘

     概要を見る

    本研究では、再帰呼び出しや割り込みなどの手続き呼び出しを持つ高レベル言語で記述された実時間プログラムの振舞いをモデル化するNested Timed Automaton(以下NeTA)を提案し、到達可能性が決定可能であることを示し、安全性検証が可能であることを示した。NeTAは、時間オートマトンをスタックアルファベットに持つプッシュダウンシステムである。さらに、時間オートマトンがスタック上にあるときにクロックを凍結する機構を導入しても、一定の条件のもとで到達可能性が保存することを示した。さらに、効率的なゾーン構成による検証手法について検討した。

  • 高階プログラムのための時相論理仕様検証

    日本学術振興会  外国人特別研究員(欧米短期)事業

    研究期間:

    2013年
     
     
     

    寺内 多智弘, Eric Koskinen

  • 量的情報流の正確な検証

    日本学術振興会  科学研究費助成事業 若手研究(B)

    研究期間:

    2011年
    -
    2013年
     

    寺内 多智弘

     概要を見る

    量的情報流の困難性に関する研究を行い、beliefやmin entropy channel capacityなど様々な情報理論的尺度に基づく量的情報流に関する検証・推論問題の困難性を解明した。計算量理論的困難性のみならず、「hyperproperty」と呼ばれるプログラム検証問題の分類を用いての困難性も考察した。また、ソフトウェアモデル検査技術と#SATソルバ等カウンティングアルゴリズムを応用した高精度な量的情報流上限検証・推論アルゴリズムを提案した。また、検証アルゴリズムの基礎となるソフトウェアモデル検査技術の改良に関する研究を行った。

  • ソフトウェアの安全性向上のための型理論の深化と応用

    日本学術振興会  科学研究費助成事業 基盤研究(A)

    研究期間:

    2008年
    -
    2010年
     

    小林 直樹, 五十嵐 淳, 住井 英二郎, 松田 一孝, 寺内 多智弘

     概要を見る

    本研究では, ソフトウェアの信頼性向上のため, これまで研究代表者らが提案してきた型に基づくプログラム検証手法を実用レベルに引き上げるとともに, 検証手法の開拓を目標としていた. 前者の主な成果として, Cプログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.

  • 型理論と線形計画法によるマルチスレッドプログラムの安全性検証

    日本学術振興会  科学研究費助成事業 若手研究(B)

    研究期間:

    2008年
    -
    2010年
     

    寺内 多智弘

     概要を見る

    本研究は、線形計画法と型理論を応用した、並行ソフトウェアの安全性(例えば、レース状態が起こらないなど)を静的(つまりコンパイル時に)検証する研究である。具体的には「分数権限計算」(FractionalCapability Calculus)という新しい概念を含んだ型システムを構築し、型推論問題を線形計画問題に帰着することにより高速に自動ソフトウェア検証を行う。

▼全件表示

 

現在担当している科目

▼全件表示

 

学内研究所・附属機関兼任歴

  • 2022年
    -
    2024年

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