Trustworthy Software: When Computers Serve as Proxies for Humans

摘要

This report shows the feasibility of rebuilding the infrastructure of embedded system software from the ground up, with trustworthiness as a fundamental premise. Specifically, we proposed to develop a collection of both domain-specific and general purpose abstract machines, languages and tools that have built-in formal methods, and develop new ones based on sound mathematical principles. We will treat hardware, operating systems, networking, and programming languages with the same methodology, ensuring their seamless integration with respect to formal system properties. We propose to develop these ideas into a prototype proof-of-concept computing system built form the ground up with the concern for trustworthiness.