Type Theory for Software Safety

软件安全的类型理论

基本信息

批准号：
17300003
负责人：
KOBAYSHI Naoki
金额：
$ 7.78万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (B)
财政年份：
2005
资助国家：
日本
起止时间：
2005 至 2007
项目状态：
已结题

项目摘要

The purpose of this project was to enhance software verification techniques based on formal methods such as type theories. The primary goal was to refine and extend our previous type-based verification techniques so that they can be used for verification of realistic programs.The main results are summarized as follows. For each topic, we have implemented a prototype verification system and confirmed the effectiveness of the verification technique.1. Verification methods for functional programsA main shortcoming of our previous type-based technique for resource usage verification was that it did not properly handle advanced language mechanisms such as exceptions. We have extended the previous resource usage verification technique to deal with exceptions. We have also devised an (incomplete) algorithm to infer dependent types, to enable automatic but more precise program analysis than previous methods.2. Verification methods for concurrent programsThe main shortcomings of our previous verification method were that it was too imprecise and that it did not handle some common primitives such as reference cells and interrupts. To address the former issue, we have integrated our previous type-based method with model-checking techniques. For the latter issue, we have developed verification methods for a C-like language with interrupts and reference cells.3. Information Flow AnalysisWe have integrated a type-based technique for information flow analysis with a mode-checking technique. The resulting analysis is more precise than previous type-based techniques, and more efficient than previous model-checking techniques for information flow analysis.

该项目的目的是增强基于形式化方法（例如类型理论）的软件验证技术。主要目标是完善和扩展我们之前的基于类型的验证技术，以便它们可以用于验证实际程序。主要结果总结如下。对于每个主题，我们都实现了原型验证系统并确认了验证技术的有效性。 1．函数式程序的验证方法我们之前基于类型的资源使用验证技术的一个主要缺点是它没有正确处理异常等高级语言机制。我们扩展了之前的资源使用验证技术来处理异常。我们还设计了一种（不完整的）算法来推断依赖类型，以实现自动但比以前的方法更精确的程序分析。2。并发程序的验证方法我们之前的验证方法的主要缺点是太不精确，并且它没有处理一些常见的原语，例如引用单元和中断。为了解决前一个问题，我们将之前基于类型的方法与模型检查技术集成起来。对于后一个问题，我们开发了带有中断和引用单元的类C语言的验证方法。3．信息流分析我们将基于类型的信息流分析技术与模式检查技术集成在一起。由此产生的分析比以前基于类型的技术更精确，并且比以前用于信息流分析的模型检查技术更有效。

项目成果

期刊论文数量（0）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Inferring Channel Buffer Bounds via Linear Programming

通过线性规划推断通道缓冲区界限

DOI：
发表时间：
2008
期刊：
Proceedings of the 17th European Symposium on Programming(ESOP'08) 4960
影响因子：
0
作者：
Tachio Terauchi;Adam Megacz
通讯作者：
Adam Megacz

A bisimulation for dynamic sealing

DOI：
10.1145/964001.964015
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
0
作者：
Eijiro Sumii;B. Pierce
通讯作者：
Eijiro Sumii;B. Pierce

計算資源使用法検証における計算資源の仕様と実際の使用法の間の適合性検証アルゴリズム

计算资源使用验证中计算资源规格与实际使用情况的兼容性验证算法