Type Systems for Secure Computing

本研究项目的目的是研究基于类型的程序验证方法。主要研究结果总结如下：并发程序的通信行为分析系统并发程序的缺陷和安全漏洞往往存在于通信描述中。我们已经开发了用于静态检测此类缺陷（例如，死锁、活动锁和竞争条件）的类型系统。计算机程序访问各种资源，如文件、内存和网络。我们已经开发了用于静态验证这些资源是否被正确访问的类型系统。例如，我们的类型系统可以验证已打开的文件是否最终关闭。信息流分析的目的是静态地检查程序是否泄露机密数据（如密码）的机密信息。我们开发了用于低级语言和并发语言的信息流分析的类型系统。我们使用证明辅助Coq对部分AnZen邮件服务器的正确性进行了形式化和验证。在此基础上，我们还构建了一个用于验证并发程序的Coq库。

The aim of this research project was to study type-based methods for verification of programs. The main results are summarized as follows.-Type sytems for analyzing communication behavior of concurrent programs Flaws and security holes of concurrent programs often reside in description of communications. We have developed type systems for statically detecting such flaws (e.g., deadlock, livelock, and race conditions).-Type systems for resource usage analysis Computer programs access various resources such as files, memory, and network. We have developed type systems for statically verifying that those resouces are properly accessed. For example, our type system can verify that a file that has been opended is eventually closed.-Type systems for information flow analysis The purpose of information flow analysis is to statically check that programs do not leak secret information about secret data such as passwords. We have developed type systems for information flow analysis for low-level languages and concurrent languages.-Verification of concurrent programs using proof assistant Coq We have formalized and verified the correctness of a part of AnZen mail server using proof assistant Coq. Based on that experiment, we have also constructed a Coq library for verifying concurrent programs.