============================================================================= Title: Applications of Logic in Computer Security Speaker: Jon Millen, SRI International Computer Science Laboratory E-mail: millen@csl.sri.com Abstract: Logics have had both direct and indirect roles in the modelling and analysis of secure systems, including operating systems and Internet protocols. Traditional mathematical logic supports the construction of general-purpose verification environments used in this area. Specialized modal logics have been used to model and verify authentication protocols and schemes for authentication and delegation using digital signature certificates. ============================================================================= Title: An Introduction to Proof-Carrying Code Speaker: Amy Felty School of Information Technology and Engineering University of Ottawa E-mail: afelty@site.uottawa.ca Proof-carrying code (PCC) is an application of formal logic and formal proof that provides a mechanism which allows a host, or code consumer, to safely run code delivered by an untrusted code producer. The host specifies a safety policy as a set of axioms and inference rules. The code producer delivers both a program and a formal proof that verifies that the code meets the desired safety policies. PCC safety policies typically include properties that prohibit the code from harmful behavior such as accessing private data, overwriting important data, accessing unauthorized resources, or consuming too many resources. Ideally, a proof is constructed automatically, and proof search may be directed using information that is passed on from the code producer's compiler. Proofs provided semi-automatically or interactively using a proof assistant are possible as well. Upon receiving the code and proof, the code consumer uses a mechanical proof checker to check the proof before executing the code. A principle advantage of this approach to software safety is that the trusted code base is extremely small; it includes only the proof checker for verifying the proof of safety. This talk will present an overview of PCC, and also introduce our approach to PCC, called foundational proof-carrying code, which provides increased security and greater flexibility in the construction of proofs of safety. ============================================================================= Title: Binding Logic: proofs and models Speaker: Gilles Dowek, INRIA France (joint work with The're`se Hardin and Claude Kirchner) E-mail: Gilles.Dowek@inria.fr In many applications of logic to computing science, we need to construct theories where some parts of mathematics can be formalized, not only in principle, but also in facts. To this end, usual frameworks such as predicate logic and set theory require slight modifications. For example, it may be useful to be able to distinguish proofs that require a genuine deduction and those that require just a computation. It may be also useful to be able to express terms in a language that allows variable binding, like the "informal" language of mathematics. In this talk, we will define an extension of predicate logic where variables can be bound in terms and in propositions. We will introduce a notion of model for this logic and we prove a completeness theorem. Finally, we will give simple examples of independence results that can be obtained with such models. ============================================================================= Title: Formal Verification of Mathematical Algorithms Speaker: John Harrison, Intel Labs E-mail: johnh@ichips.intel.com An important feature of typical computer systems is the computation of basic mathematical functions, mainly in floating-point arithmetic. This includes basic arithmetic operations like division, as well as common transcendental functions like "exp" and "sin" and more obscure ones like gamma and Bessel functions. Since they often depend on some non-trivial mathematics and subtly exploit the special features of floating-point operations, they are relatively difficult to design without error. The costs to a company like Intel of a failure, especially at the hardware level, can be huge. For example, the error in the FDIV (floating-point division) instruction in early Pentium processors in 1994 is believed to have cost Intel about $500M. We will describe our work at Intel on the formal verification of some mathematical algorithms that are implemented in microcode and in software libraries on some of Intel's current and forthcoming processors. The work uses the HOL theorem prover, a programmable interactive proof checker for classical higher-order logic. We will describe how a body of classical mathematics (e.g. elementary real analysis) is completely formalized in HOL, and applied to typical applications, exploiting programmability. HOL has the unusual feature of explicitly generating all proofs in terms of basic low-level primitive inferences of the kind typically considered in proof theory. Some of the algorithm verifications involve of the order of 100 million primitive inferences. This can be seen as a realization of the "Principia Mathematica" ideal of actually doing proofs using simple proof systems --- with the help of the computer.