With the recent advances in network computing, it has become quite common for a program produced by one host to be sent to and executed by others. This situation has created a demand for new technologies that can protect computers from unreliable and possibly malicious foreign programs transmitted by untrusted hosts.
How can we produce, transmit, and execute only those programs that can be proven to be safe? This question motivates the study of the framework of provably safe software distribution.
This framework can be divided into the three main phases (Fig. 1). The first phase concerns the production of correct and safe source programs from specifications including safety policies, the second the compilation of programs with their safety proofs into native machine codes (or architecture-neutral virtual machine codes) with their corresponding safety proofs, and the third the transmission of machine codes with their lengthy safety proofs in a feasible manner, or in other words, a method of efficiently convincing each code consumer of the safety of machine codes. There are a lot of studies on the first phase in the literature, including a type-theoretical approach to developing provably correct functional programs [1, 2]. The type-preserving translation of a high-level programming language to a typed assembly language is an example of a recent development in the second phase. The work described in [3, 4, 5, 6] concerns the third phase and presents an interactive and probabilistic extension of the proof-carrying code mechanism. We expect that our efforts will lead to a useful framework of provably safe software distribution.