serve as formal specifications for the
low-level implementation.
The stratified system model gives
programmers a systematic and principled approach for controlling complexity. Programmers can thus focus
on a subset of language features at
each level and certify different software components using specialized
program logics.
Certified and certifying compilation. Much work in the program-verification community concentrates on
source-level programs written in high-level languages (such as C, Java, and
C#). In order to turn these programs
into certified assembly components
suitable for linking in the OCAP framework, OCAP developers must show
that their corresponding compiler is
also trustworthy.
CompCert is a certified compiler
for a subset of C (called C minor, or
Cm) developed in 2006 by Leroy. 20 By
“certified” compiler, I mean the compiler itself is proved correct. Indeed,
Leroy specified formal operational semantics for Cm, as well as for the machine language, building a machine-checkable proof in Coq whereby the
compiler preserves behavior from
one operational semantics to another.
However, the current CompCert compiler supports only sequential Cm programs. It also must be bootstrapped by
the OCaml compiler, even though the
OCaml compiler is not verified.
On the other hand, a certifying
compiler is not necessarily correct but
will take a (certified) source program
and generate certified assembly code.
Much work on certifying compilation
focuses on type-safe source languages
and can preserve only type-safety properties. A challenging open problem
is to extend certifying compilation to
preserve deep correctness and security
properties.
Lightweight formal methods.
Building large-scale certified software
systems does not always require heavy-
weight program verification. Most
software systems are built from modu-
lar components at several levels of ab-
straction. At the lowest levels are the
kernel and runtime-system compo-
nents discussed earlier. At the highest
levels are components with restricted
structure operating on well-defined in-
terfaces. The restricted structure can
use a type-safe, high-level program-
ming language with high-level concur-
rency primitives or C programs (even
concurrent C programs) in a style un-
derstandable to static-analysis tools.
Both restricted styles are in wide-
spread commercial use today.
Much previous research on verification reflected full automation as a
dominating concern and was reasonable if the primary goal is finding bugs
and having an immediate effect on
the real world’s vast quantity of running software. Unfortunately, insisting on full automation also severely
hinders the power and applicability
of formal verification; many interesting program properties (that end users
care about) are often undecidable (full
automation is impossible), so human
intervention is unavoidable. Low-level
program modules often have subtle
requirements and invariants that can
be specified only through high-order
logic; programming libraries verified
through first-order specifications often have to be adapted and verified
again at different call sites.
Nevertheless, there is still great
synergy in combining these two lines
of software-verification work. The
OCAP framework described earlier
emphasizes domain-specific (
including decidable first-order) logics to
certify the components in a software
system. Successful integration would
allow programmers to get the best of
both lines.
Developing large-scale mechanized
proofs and human-readable formal
specifications will be an exciting research field on its own, with many
open issues. Existing automated theorem provers and Satisfiability Modulo
Theories solvers6 work on only first-order logic, but this limited functionality
conflicts with the rich metalogic (often
making heavy use of quantifiers) required for modular verification of low-level software. Proof tactics in existing
proof assistants (such as Coq) must be
written in a different “untyped” language, making it painful to develop
large-scale proofs.
Conclusion
Certified software aligns well with a
2007 study on software for dependable
systems18 by the National Research
Council ( http://sites.nationalacade-mies.org/NRC/index.htm) that argued
for a direct approach to establishing
dependability, whereby software developers make explicit the dependability
claim and provide direct evidence that
the software indeed satisfies the claim.
However, the study did not explain