Theory Challenges

***** SUPERSEDED by Outline of Theory Challenges *****

Logics for sequential imperative programs

Here we use ``axiomatic semantics'' loosely, to mean program logic, weakest precondition calculus, refinement calculus, or similar formal systems for correctness of programs with respect to pre-post specifications, intermediate assertions, and relational formulae. On one hand, axiomatic semantics should be validated in terms of models faithful to actual implementation (compiler, runtime system, instruction set). On the other hand, it serves to embody general rules of reasoning in a form that facilitates specification and reasoning about particular systems. Axiomatic semantics can also serve as basis for notions of program equivalence and refinement since it abstracts from details that may not be considered observable.

Sequential code in commonly used languages like C and Java involves language features and design idioms pose problems for specification and verification not fully solved to date:

• code pointers (Must first-order specifications be abandoned? Can the problems with denotational semantics of stored procedures, vs procedures as arguments as in Algol, be dodged to get good proofsystems?
• modular specification and reasoning with frame conditions (term? or modifies specs?) for mutable heap structure (can separation logic be extended to richer data model and language features? relationships between ownership systems?)
• inheritance---frame conditions for extended state in subtypes, dynamically bound method calls and behavioral subtyping for reasoning in terms of static types
• inline assembler, which exposes aspects of machine semantics that in well designed programs are carefully isolated
• reentrant callbacks
• address arithmetic, or alternatively the abstraction/security properties obtained by disallowing address arithmetic
• use of ``pure'' program expressions in specifications

The literature offers solutions to individual problems under simplifying assumptions.

Challenge: Integrate some solutions to produce a proofsystem or semantics adequate for verifying interesting challenge codes. Develop a semantic model and verify soundness of the proofsystem (meta-theory which merits machine checking, as the point is to include a number of complicated language features) Such an integration is being attempted in JML.

For some purposes it is important to verify bytecode or other unstructured code, and several groups have shown this can be achieved less frightfully than might be expected (see for example the JBook).

To-do: links to Mobius project, Spec#, Tan and Appel, what?

System modeling and programming notations

Some of the discussion in the Correct by Construction panel is concerned with designing languages to take verification into account. Do we know which features of current languages really need to be changed because they have severe and avoidable repercussions (which should be apparent from the theory), vs superficial aspects which result in minor engineering complications for verification tools?

Better still, can we fulfil the dream articulated by Hoare (``Varieties of programming language'', unifying theories), Abrial (at the VSTTE meeting) and many others for a long time: rather than a fixed ``language'', a program should be specified and implemented using a selection of notations suited to the particular system. Theory should account for reasoning principles associated with these notations and in particular guide the design of sound tools, no more complex than necessary for the particular selection of notations.

Here the relevant theory is not just semantics for programs / designs / requirements models but also logic, e.g., for sound scripting of integrated proof techniques using decision procedures etc.

Reynolds' Idealized Algol is a good example of combining two sorts of notations in a way that retains many properties for reasoning etc. Boerger's incremental development of Java similarly builds relatively orthogonal layers. How close are these examples to Abrial's engineering considerations; is smaller granularity of language features needed? what about "features" in the sense of restricted forms of constructs, e.g. linear or affine lambda terms, threads with bounded or disjoint heap.

The decomposition and modularization techniques needed here have to support the analysis of run-time features; logical structure alone is insufficient to guide the separation of different concerns engineering needs force us to make explicit. Good theoretical concepts for decomposition and modularization that take behavioral aspects into account are still a challenge.

Challenge: The refinement generator challenge consists in defining practical model refinement schemes, which capture established system development and programming knowledge, together with justifications of their correctness. Where the refinement process is highly creative, interactive schemes can still be helpful to guide the refinement process by a combination of user-insight and mechanized tactics. In particular, these refinement schemes should allow the verifier to turn model properties into software interface assertions comprising behavioral component aspects, to be used where state-based run-time features are crucial for a satisfactory semantically founded correctness notion for code.

Challenge: The refinement verifier challenge is to enhance current computer-based verification systems by means to prove the correctness of practical model refinement schemes.

Challenge: The refinement validator challenge consists in linking the refinement of ground models to model simulators to make the generation and systematic comparison of corresponding test runs of abstract and refined machines possible. In particular relating system and unit level test results should be supported by this enhancement of model simulation tools.

Challenge: A runtime verifier challenge consists in instrumenting current high-level model execution tools (e.g. interpreters for ASMs or event-B models or model checkers for TLA+ models) to monitor the truth of selected properties at runtime, enabling in particular the exploration of ground models to detect undesired or hidden effects or missing behavior.

Challenge: A re-engineering method milestone is to define methods to extract ground models from legacy code as basis for analysis (and re-implementation where possible.

Concurrency

To-do: Dave nominated Peter O'Hearn to develop this topic.

There are numerous abstract models of concurrency suitable for requirements and design specification.

For verification of code, however, we need good semantics for shared-memory concurrency with weakly consistent memory models. Lock-free programs and transactional memory appear promising and important.

We should be able to formulate good challenges here for axiomatic and other semantics. This may require fundamental advances in semantics and initial results for idealized languages. Machine checking does not seem essential.

Certifying compilation

To-do: Dave nominated Markus Mueller-Olm and Xavier Leroy to develop this topic.

Does the deployment model of ``proof carrying code'' have special interest or is the more general problem that reasoning tools exchange witnesses?

Compiler verification

To-do: Dave nominated Xavier Leroy and Markus Mueller-Olm to develop this topic.

Building proven to be correct compilers for real-life languages and target machines (using prover-based theoretical methods and development tools).

Proving existing compilers to be correct. As part of this challenge one may consider the further development of proof carrying code methods to make them fit real-life languages. (An example is the certifying compilation using type carrying code developed for the completeness proof of Java compilers with respect to the JVM bytecode verifier, see Ch.16.5 of the Jbook.)

Milestone Verify by existing mechanical theorem proving systems the following theorems proved in the Jbook for abstract interpreters of Java and the JVM defined there: 1. Java is type safe (Thm.8.4.1) 2. Correctness of the Java2JVM compilation scheme (Thm.14.1.1) 3. JVM Invariants for soundness of Bytecode Type Assignments (Thm.16.4.1) 4. Completeness of the scheme for certifying Java2JVM compilation (Thm.16.5.1,16.5.2) * 5. Soundness of the bytecode verifier (Thm.17.1.1)

Type systems

To-do: Dave nominated Steve Zdancewic to develop this theme and perhaps others pertaining to mechanized meta-theory.

Correctness of multistage notations

Peter Sestoft develops this theme.

This section has relations to correctness of code generation and compilation; but its specific focus is programmer-controlled generation of program code and documents. A lot of one-time effort can (and should) be invested in proving a compiler correct, and in creating compilers that generate code along with a proof of its correctness. This section is about improving the reliability of the thousands of more ad hoc generators written every week by practitioners.

Theoretical foundation for moving away from the classical static compile-link-run model of language semantics to where meta-programming, generative programming, model-driven development, and multistage programming are leading, namely to work with VM-based (interpreted or compiled) managed code and managed execution. Here programs are generated from code patterns, code fragments written in different languages and/or components according to directives expressed through metadata, instantiating a general problem solution to particular cases of the problem. What we need is a practical theory that brings generative programming techniques, which at present are mostly embedded in some tools or language features, under the explicit control of the programmer, providing means to control the structure and the semantical content of generated code. Also partial evaluation techniques belong here.

List of topics to consider:

• More and more code is generated rather than written. By code we mean here first and foremost source code in a higher programming languages, but also GUI descriptions, deployment descriptors, database queries, hyperlinked documentation, web pages, Javascript code embedded in web pages, and so on. The tools and notations used to write the code generators often do not provide even the most elementary guarantees that the generated code is correct.
• Generated code may be checked for correctness on at least four levels: (a) Syntactic well-formedness; (b) Scope well-formedness (when the generated code contains variable binders, cross-references and similar); (c) type correctness (when the generated notation has a static notion of type); and (d) dynamic semantics correctness -- does the generated code mean or do what it is intended to?
• Static correctness guarantees are particularly important for runtime code generation, where a system may fail at runtime due to the faulty generation of code. For code generated at compiletime or build time, a compilation phase will usually check at least correctness (a), (b) and (c) before deployment is attempted, but this is not necessarily the case for code generated at runtime.
• One can even consider runtime "hardware" generation: there are now systems that include FPGA boards, so one can create and configure a specialized co-processor at runtime. Such systems are rather hard to debug, so static guarantees are highly desirable.

  (TODO: Fix layout; this is not part of the bullet) Relevant work and people include: Staged computation (Joerring and Scherlis, Lisp/Scheme quasiquotation (backquote and comma), DynJava (Oiwa), MetaML (Sheard), MetaOCaml (Calcagno, Leroy, Taha), Metaphor (Neverov, Roe), dependent types (Martin-Lof, Coquand), the Coq system, Omega (Sheard), Pasalic, Linger, Pfenning, Davies, Nanevski, Pitts, Nielson, Batory, Czarnecki, Smaragdakis, Kamin, explicit substitutions, ... Some relation to model driven development.

  Challenge: Develop a theory of types for multistage languages that covers correctness levels (a), (b), (c) and (d). The theory should support type notations and mechanized consistency checking. Relevant existing theory includes dependent types (Martin-Lof) and nominal logic (Pitts).

  Challenge: Develop a theory of types for runtime reflection.

  Challenge:

Verified secure flow checker

Barthe and Rezk give an iterative analysis for determining a security labeling bytecode with respect to a given security policy for a program's public API. Here a policy consists of assignment of levels in a lattice to the public methods, fields and global variables. The analysis has been proved sound in the sense that accepted programs are noninterferent in accord with the policy, where noninterference means absence of influence in terms of a standard semantics in which timing, power consumption, resource exhaustion and othe covert channels are not modeled.

For bytecode generated by a compiler, the compiler can produce this labeling. The rules have been simplified to rules for checking a given labeling and exploiting properties of compiled code, e.g., the operand stack is empty at control points corresponding to control points in the source code.

Challenge: Give a machine-checked proof of noninterference for the revised system. This involves a semantics for bytecode, specification of the analysis, quantification over all programs, and the noninterference property which has the form of a logical relation or simulation (property of not one but two executions).

If the analysis is specified in a form that is executable, such as the functional program in Naumann's verification of a source level checker in PVS~\cite{naumann-tphols05}, then this could be considered a verified program rather than verified meta-theory. But for practical deployment an implementation would at least need glue code in addition to the pure PVS functions; most likely a bytecode checker for production use will be implemented in a subset of C, possibly compiled with optimizations or linked with hand written assembler.

Challenge: Verify an implementation of this analysis with respect to its full functional specification, i.e., accepted bytecode is noninterferent. The obvious proof strategy would be to rely on the noninterference result for an abstract description of the analysis (previous challenge item): prove that the implementation simulates the abstract program in a suitable sense. This involves semantics of both the implementation language and the ``specification language'' in which the abstract program is expressed. An alternative to carrying out the simulation proof directly in terms of the semantics would be a more ``axiomatic'' approach; e.g., using an assertion-based program logic (in which components of the abstract program might be admissible as terms), or using equivalence preserving transformations.

An input to the bytecode analysis is a sound approximation of the program's control dependence regions (to track flow of information via control flow). An implementation of the analysis should include a check that the regions are correct (a high level implementation has been machine checked in Coq by Barthe). But regions are used for other purposes, in particular, optimizing transformations. The challenge can be embellished by including optimization and asking that the region analysis be treated as a component so, in particular, its specification is sufficiently strong and general to cater for these multiple purposes.

Bytecode optimization also entails adapting the security analysis. Can verification of the original analysis be adapted to one that handles some important optimizations? Or to an algorithm for finding regions and finding security labeling? Can the properties proved be re-used, or the proof techniques and ancillary results?

Finally, the bytecode labeling is produced by the compiler based on information from a source level analysis. Security of the bytecode does not depend on correctess of the compiler but it is desirable that source code deemed secure by the source level analysis compiles to bytecode that is accepted. This has been proved on paper via a slightly intricate technique which the authors claim can be used to cater for additional language features and more sophisticated security policies.

Challenge: Formulate the source level analysis and label-generating compiler. Machine-check a proof that accepted source code compiles to accepted bytecode. Extend the language and policies; adapt the proof.

Challenge: Extend this to certifying compilation.

Modularity reasoning and data structures

Automated verifiers have difficulty with data structures because relevant conditions often involve quantification over nodes reached by pointer paths. One means to lessen the problem is to distribute conditions over the structure. For example, a heap-ordered tree can be described by: (a) each node's value exceeds that of all its descendants, or (b) each node's value exceeds that of its children. That (b) implies (a) can be justified offline so that (a) is used in the annotation. More to the point, version (a) sounds like a quantifiaction over nodes --the quantified formula would be associated with the root object perhaps. An alternative is for each node to maintain an invariant that it's value exceeds that of its children. The quantification is thereby lifted to a global statement that all object invariants are maintained.

This approach has been explored in the context of object-oriented source programs (Leino, Mueller, ...) with the attendant baggage such as concern with inheritance, focus on encapsulation, ownership, and other notions tied to OO syntax. Separation logic offers an attractive way to delimit the dependence of predicates, but extant examples make heavy use of predicates defined inductively. One can imagine invariants with dependence circumscribed not by syntactic considerations but by small bounds on the length of pointer chains to be followed.

Challenge Is there a more general theory of predicates with circumscribed dependence on the heap, to generalize previous work and more importantly to facilitate use in tools? Can circumscription of dependence be measured by size of footprint, to facilitate algorithms doing bounded search for quantifier free properties?