Proof-Carrying Code for Verifying Confidentiality of Mobile Code through Secure Information Flow Analysis

The growing dependence of our society and economy on networked information systems makes it essential to protect our confidential data from being leaked by malicious code. Downloading and executing code (possibly from untrusted sources) has become a daily event. Modern operating systems load code for adding new functionalities; web browsers download plug-ins and applets; end-users download untrusted code for doing some useful tasks. Certification that the untrusted code respects the confidentiality of data it manipulates is essential in these situations. Thus it is necessary to analyze how information flows within that program. This thesis presents an approach to enable end-users to determine whether untrusted mobile code will respect pre-specified confidentiality policies by statically analyzing the untrusted code for secure information flow. The approach is based on adapting of a well-known approach, proof-carrying code (PCC) to information flow security and basing the security policy of PCC on a security-type system, which enforces information flow policy, namely noninterference security policy in RISC-style assembly programs. The untrusted code is then analyzed for secure information flow based on the idea of PCC. The proofs that untrusted code does not leak confidential information are generated by the code producer and checked by the code consumer. If the proofs are valid, then the end-users (code consumer) can install and execute the untrusted mobile code safely. The proposed approach benefits from distinctive features that make it a very appropriate for security checking. First, it operates directly on object code produced by general-purpose off-the-shelf compilers. Second, it exploits the benefits that both type systems and proof-carrying code approaches offer and combines their strengths. Type systems provide an appealing option for implementing security policies, and thus represent a natural enabling technology of proof-carrying code. Meanwhile, proof-carrying code is an efficient approach for assembly code verification. Third, the explicit machine-checkable proofs serve as a certificate to distrustful users and give them more confidence in the security approach. The proposed security approach represents one point in the design space for mobile code security systems; it is well suited to typical Internet users. It enforces information flow policy with low preparation cost on the part of the code producer and no runtime overhead cost on the part of the code consumer. The security approach provides end-users with an adequate assurance of protecting the confidentiality of their confidential data