concern in the context of mobile code.
An important PCC advantage inherited by certified software is that the
software does not require a particular
compiler. As long as the code producer
provides the proof, the code consumer
is assured of safety. This significantly
increases the flexibility available to
system designers.
The PCC framework is itself quite
general, but the original PCC systems
suffered from several major limitations: Most notable was that the proof
checker had to rely on a rather specific
set of typing rules so did not support
more expressive program properties;
the typing rules were also error-prone,
with their soundness often not proved,
so a single bug could undermine the
integrity of the entire PCC system.
Foundational PCC, or FPCC, 1, 13
tackled these problems by constructing and verifying its proofs using a
metalogic, with no type-specific axioms. However, FPCC concentrated on
building semantic models for high-level type-safe languages, rather than
performing general program verification.
Certified assembly programming.
CAP32 is a logic-based approach for
carrying out general program verification inside a rich mechanized
metalogic (such as the one provided
by Coq). Like Hoare logic, a CAP program consists of assembly code annotated with pre- and post-conditions
and program invariants. Unlike traditional Hoare-style verification, all
CAP language constructs (such as assembly instruction sets), program assertions, inference rules, operational
semantics, and soundness proofs
are implemented inside the mechanized metalogic. This design makes
it possible to build a complete certified software package with formal
dependability-claim and machine-checkable proofs. With help from a
proof assistant, programmers are able
to combine manually developed proof
scripts with automated proof tactics
and theorem provers, allowing CAP to
support verification of even undecidable program properties.
CAP marries type-based FPCC with
Hoare-style program verification, leading to great synergy in terms of modularity and expressiveness. Hoare logic
is well known for its limited support
machine-
checkable proofs
are necessary
for allowing third
parties to quickly
establish that a
software system
indeed satisfies
a desirable
dependability claim.
for higher-order features; most Hoare
systems do not even support verification of simple type-safety properties.
However, both shortcomings are easily overcome in type-based approaches. Subsequent work on CAP over the
past five years developed new specialized program logics for reasoning
about such low-level constructs as embedded code pointers, 24 stack-based
control abstractions, 10 self-modifying
code, 3 and garbage collectors. 21
Under type-based FPCC, function
returns and exception handlers are often treated as first-class functions, as
in continuation-passing style (CPS),
even though they have more limited
scope than general first-class continuations. For functional programmers,
CPS-based code is conceptually simple but requires complex higher-order
reasoning of explicit code pointers
(and closures). For example, if a function needs to jump to a return address
(treated as continuation), the function
must assert that the return address is
indeed a valid code pointer to jump to.
But the function does not know exactly
what the return address will be, so it
must abstract over properties of all
possible return addresses, something
difficult to do in first-order logic.
In our work on stack-based control abstraction, 10 my colleagues and
I showed that return addresses (or exception handlers) are much more disciplined than general first-class code
pointers; a return address is always
associated with some logical control
stack, the validity of which can be established statically; a function can cut
to any return address if it establishes
the validity of its associated logical
control stack. Such safe cutting to
any return address allows programmers to certify the implementation of
sophisticated stack operations (such
as setjmp/longjmp, weak continuations, general stack cutting, and context switches) without resorting to
CPS-based reasoning. For example,
when programmers certify the body
of a function, they do not need to treat
its return address as a code pointer;
all they need is to make sure that at
the return, the control is transferred
to the original return address. It is the
caller’s responsibility to set up a safe
return address or valid code pointer;
this is much easier because a caller