QCPLS, abstracts, Avril 2004


Foundational Proof-Carrying Code

Amy Felty, School of Information Technology and Engineering, University of Ottawa

Proof-carrying code (PCC) provides a mechanism for insuring that a host, or code consumer, can safely run code delivered by a code producer. The host specifies a safety policy as a set of axioms and inference rules. In addition to a compiled program, the code producer delivers a formal proof of safety expressed in terms of those rules that can be easily checked. 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. In addition, the safety properties of interest are much easier to prove automatically than general program correctness. This talk will focus on our approach to PCC, called foundational proof-carrying code, which provides increased security and greater flexibility in the construction of proofs of safety.

Information about a particular programming language, such as the type system, is essential in constructing proofs of safety. One way to include such information is by adding new inference rules to the base logic. This approach requires a different proof checker for each programming language, and even for each compiler. In foundational PCC, proofs of safety are constructed from the smallest possible set of axioms and inference rules. Types are modeled via definitions from first principles and the typing rules are proved as lemmas. All definitions and lemmas used in a particular proof are included inside it. Thus a single proof checker can check safety proofs for any programming language for which typing lemmas have been proven. Also, since the set of inference rules is smaller, the proof checker is simpler, and thus the trusted code base is smaller.


History Types and Verification

Christian Skalka, University of Vermont

Safe program execution is crucial for modern information systems, but is difficult to attain in practice. Both faulty logic, due to programmer errors, and access control violations, due to intentional attacks, can lead to unsafe program executions. Programming language-based tools and techniques can increase safety by verifying at both compile- and run-time that programs possess certain safety properties.

This presentation describes a new foundation for static verification of program properties, built on a novel process for automatically extracting event histories of program executions, and for specifying and automatically verifying properties of these histories. Our approach combines a type and effect theory with model checking techniques, which is expressive enough for application to a range of static analyses; in particular, we will discuss language-based access control as an application focus.

This is joint work with Scott Smith, Johns Hopkins University.


Towards an improved Java bytecode verifier

Étienne Gagnon, Université du Québec à Montréal

Java programs are compiled to a platform-independent bytecode instruction set. A nice property of programs in bytecode format is that they can be subjected to a link-time verification process which detects and rejects violations to static and structural constraints of the Java virtual machine.

In this talk, we will first present some limitations and holes in the current verification algorithm found in the Java virtual machine specification such as the failure to protect against some invalid field assignments, missing verification of primitive types, and missing verification of structured locking. Then we will discuss our plans for improving the Java verifier by fixing its holes, improving its worst-case algorithmic complexity in presence of subroutines, and assessing of additional structural constraints.


Towards dynamic interprocedural analysis in JVMs

Feng Qian, McGill University

Reachability-based interprocedural analyses (IPAs), such as points-to and escape analysis, require a call graph of the analyzed program. There are several challenges of computing a call graph for a Java program at runtime. First, the overhead must be low. Second, both polymorphism and lazy class loading must be dealt with correctly and efficiently. In this presentation, we show how to adapt several well-known static type analyses into a Java virtual machine, and measure their effectiveness for call graph construction. We also propose a new, simple type analysis using runtime class information for computing call graphs. Then we present a new, inexpensive, mechanism using profiling code stubs for constructing a complete call graph in JVMs. Finally we provide an example of how to implement a dynamic reachability-based IPA, namely dynamic XTA.


Precise, Partially Compositional Analysis of the pi-Calculus

Sam Sanjabi, McGill University

We present a new algorithm for computing control flow analysis on the $\pi$-calculus. Our approach is strictly more accurate than existing algorithms, while maintaining a polynomial running time. We also explicitly consider the {\em replication} operation, and are thus able to analyze the full $\pi$-calculus. Complete results can be obtained for fully-specified process definitions, and we achieve partial compositionality for open processes through reuse of internal data structures.


Burger Lazy-Scheme : Réduction de Graphe en Parallèle sur FPGA

Étienne Bergeron, Université de Montréal

La réduction de graphe est une technique d'évaluation de langage paresseux qui a pour avantage de permettre une évaluation parallèle, distribuée et spéculative.

Dans notre projet, nous proposons un compilateur d'une version paresseuse de Scheme et une implantation d'un réducteur de graphe parallèle sur une architecture reconfigurable.

Le compilateur transforme le langage fonctionnel en combinateurs et produit le code effectuant les ré-écritures de graphe pour ces combinateurs. Un processus de réduction de graphe en matériel exécute le code produit sur une architecture possèdant des primitives efficaces pour l'implantation des mécanismes nécessaires à l'évaluation parallèle et spéculative. Cette architecture possède des primitives telles que des allocations atomiques de paires et un GC concurrent "on-board".

Dans notre présentation, nous ferons un survol de ce qui est présentement réalisé et de nos intentions futures sur ce projet.


Stefan Monnier
Viewable With Any Browser