Type Systems for Secure Computing

点击翻译按钮获取中文摘要

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.