contributed articles
Doi: 10.1145/1859204.1859226
Only if the programmer can prove (through
formal machine-checkable proofs) it is free of
bugs with respect to a claim of dependability.
BY zhonG Shao
Certified
Software
CoMpUter soFt Ware is one of the most influential
technologies ever created. Software has entered every
aspect of our lives, used to control everything from
computing and communication devices (such as
computers, networks, cellphones, and Web browsers),
to consumer products (such as cameras, TVs, and
refrigerators), to cyber-physical systems (such as
automobiles, medical devices, and aviation systems),
and to critical infrastructure (such as financial,
energy, communications, transportation, and national
defense).
Unfortunately, software is also sometimes our
least dependable engineering artifact. Software
companies lack the kind of meaningful warranty
most other engineering organizations are expected
to provide. Major corporations and government
agencies worldwide invest in fixing software bugs,
but prospects for building reliable
software are bleak. The pervasive presence of software bugs also makes all
existing computing and information
systems vulnerable to security and privacy attacks.
An important cause of such difficulty is the sheer complexity of the
software itself. If each line of code is
viewed as an individual component,
software systems are easily the most
complicated things we humans have
ever built. Unlike hardware components, software execution can easily lead to an unbounded number of
states, so testing and model-checking
techniques cannot guarantee reliability. As the hardware community moves
deep into new multi-core and cyber-physical platforms, and as software is
thoroughly integrated into everyday
objects and activities, the complexity of future software could get much
worse, even as demand for dependable
software becomes more urgent.
For most of today’s software, especially low-level forms like operating systems, nobody knows precisely
when, how, and why they actually
work. They lack rigorous formal specifications and were developed mostly
by large teams of developers using
programming languages and libraries
with imprecise semantics. Even if the
original developers had a good informal understanding of the inner work-
key insights
The dependability of a software system
should be treated separately from its
execution environment; the former is a
rigorous mathematical entity, but the
latter is imperfect and far less rigorous.
Building end-to-end certified
software requires a rich metalogic for
expressiveness, a set of domain-specific
program logics for modularity and
automation, a certified linking framework
for interoperability, and machine-checkable proofs for scalability.
The trusted computing base of a good
certified framework should contain
only components whose soundness
and integrity can also be validated by
independent third parties.