🚀 go-pugleaf

                                     COLLOQUIUM

                University at Albany - State University of New York

                            Computer Science Department

                Proving Safety of Complex Operations in Mobile Code

                                     Amy Felty

                           Bell Labs, Lucent Technologies

                                    Revised Time

            Tuesday, March 23, 1999 at 4:00PM, in LI-98 (CS Conference Room)

                                      ABSTRACT

                 Proof-carrying code  (PCC)  provides  a  mechanism  for
            insuring  that a host, or code consumer, can safely run code
            delivered  by  a  code  producer.   Web  browsers  executing
            applets  from  foreign sites is one example of a domain that
            can benefit from such a mechanism.  In PCC, the host  speci-
            fies  a  safety policy as a set of axioms.  In addition to a
            compiled program, the code producer delivers a formal  proof
            of  safety  expressed  in  terms of those axioms that can be
            easily checked.  Using such an approach, the trusted comput-
            ing  base  is  extremely  small;  it includes only the proof
            checker for verifying the proof of safety.

                 I will present our work on a PCC system.   In  particu-
            lar,  I  will describe our progress toward our goals of han-
            dling a realistic  set  of  programming  language  features,
            defining  a universal safety policy that is independent of a
            particular programming language or compiler, and  addressing
            issues of scalability.

                 Our PCC system is  implemented  in  the  Lambda  Prolog
            higher-order  logic programming language.  In previous work,

                                       - 2 -

            we demonstrated that Lambda Prolog was  well-suited  to  the
            implementation  of  theorem  provers  and proof checkers.  I
            will show that the PCC application fits naturally into  this
            framework  and  illustrate  how Lambda Prolog provides addi-
            tional benefit for operations required of PCC  systems  such
            as proof optimization.

                 This is joint work with Andrew Appel (Princeton Univer-
            sity).