Provably Safe Software Distribution

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.

Three Phases

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.

Relevant References

[1] Yasuyuki Tsukada, Type-free equational reasoning in the theory of inductively defined types, in: M. Sato and Y. Toyama, editors, Third Fuji International Symposium on Functional and Logic Programming (World Scientific, Singapore, April 1998) pp. 227-246. [Abstract]

[2] Yasuyuki Tsukada, Martin-Löf's type theory as an open-ended framework, International Journal of Foundations of Computer Science, Vol. 12, No. 1 (February 2001) 31-67. [Abstract]

[3] Yasuyuki Tsukada, Mobile codes with interactive proofs, in: Proceedings of the 15th JSSST Conference (Japan Society for Software Science and Technology, September 1998) pp. 285-288.

[4] Yasuyuki Tsukada, Mobile codes with interactive proofs: An approach to provably safe evolution of distributed software systems, in: T. Katayama, T. Tamai, and N. Yonezaki, editors, 2000 International Symposium on Principles of Software Evolution (IEEE Computer Society Press, February 2001) pp. 23-27. [Abstract]

[5] Yasuyuki Tsukada, Interactive and probabilistic proof of mobile code safety, Automated Software Engineering, Vol. 12, No. 2 (April 2005) 237-257. [Abstract]

[6] Yasuyuki Tsukada, Proof hiding in interactive proof-carrying code and its applications (in Japanese), IPSJ Journal, Vol. 46, No. 1 (January 2005) 236-246. [Abstract]

Presentation

[A] Yasuyuki Tsukada, Interactive and probabilistic proof of mobile code safety, Complexity Seminar, Tokyo Institute of Technology, September 2001. [Slides (PDF)]