ware need to be verified. Already, Appel
points out, some verification tools are
commercially viable. For example, an
optimizing C compiler in France called
CompCert is being evaluated by Airbus
and European certification agencies
for use in compiling the fly-by-wire
software used to fly the Airbus jetliner.
“Compared with the compiler Airbus currently uses, CompCert has the
advantage of being proved correct, no
matter what program is compiled,”
Other aeronautics agencies are also
starting to use them. Formal verifica-
tion tools “have been shown to be ef-
fective at finding defects in safety-crit-
ical digital systems including avionics
systems,” according to a 2017 report
released by the U.S. National Aeronau-
tics and Space Administration (NASA)
Langley Research Center. Also, the U.S.
Federal Aviation Administration (FAA)
has issued guidelines that allow the
use of formal methods tools to replace
some of the methods it uses for “certi-
NASA acknowledges this will be a
slow process, noting, “There are still
many issues that must be addressed
before formal verification tools can
be injected into the design process for
digital avionics systems.” The report
points out, “Most developers of avion-
ics systems are unfamiliar with even
the basic notions of formal verifica-
tion, much less which tools are most
appropriate for different problem do-
mains,” and skills and expertise will be
needed to master the tools effectively.
The U.S. Defense Advanced Re-
search Projects Agency (DARPA) has
developed a program called High-As-
surance Cyber Military Systems that
takes a “clean-slate, formal meth-
ods-based approach to enable semi-
automated code synthesis from ex-
ecutable, formal specifications.” The
approach ensures a hacker-proof sys-
tem and “illustrates that we’re now
at a point where such systems can be
deployed in truly mission-critical envi-
ronments,” notes Jagannathan.
In recent years, the auto industry
has become aware of how vulnerable
cars are to hacking, and “they are eagerly looking for solutions from security researchers and verification
researchers,” Appel says. He believes
in the next decade there will be more
industries using software verification,
and more software available for purchase that has been verified.
For software verification to become
widespread, however, there must be
trusted compilers to translate these formal software verification methods, since
they are written in high-level languages.
Progress is being made, however, and
when a trusted compiler becomes widely available, the issue of hacker-proof
software may no longer be a wistful notion, but a concrete reality.
Certified Software, Communications of the
ACM, 53( 12), pages 56-66, December 2010
Serna-M. E., and Morales-V. D.
State of the Art in the Research of Formal
Verification, Ingeniería, Investigación y
Tecnología, Oct.-Dec. 2014, pgs. 615-623.
Volume 15, Issue 4.
D’Silva, V., Kroening, D., and Weissenbacher, G.
A Survey of Automated Techniques
for Formal Software Verification, IEEE
Transactions on Computer-Aided Design of
Integrated Circuits and Systems, July 2008,
Vol. 27, No. 7.
Souyris, J., Wiels, V., Delmas, D., and Delseny, H.
Formal Verification of Avionics Software
Products, FM 2009: Formal Methods,
Second World Congress, Eindhoven, The
Netherlands, Nov. 2-6, 2009, Proceedings,
The Verifying Compiler: A Grand Challenge
for Computing Research. In: Hedin G. (eds)
Compiler Construction. CC 2003. Lecture
Notes in Computer Science, 2003, vol 2622.
Springer, Berlin, Heidelberg
Esther Shein is a freelance technology and business
writer based in the Boston area.
© 2017 ACM 0001-0782/17/08 $15.00
proofs so the computer can check them
for every version of the system.
This can be time-consuming and
inefficient. “Ideally, if you proved one
version and made a small change, you’d
only make a small change to the proof,
but that’s not the way it works,” Tatlock
says. Whenever even a small change is
made to software code, “it can have very
large consequences,” resulting in a big
change in the proof. It might change
some fact that’s relied upon throughout
the rest of the proof, he adds.
Other techniques are less powerful,
like bounded model checking, which is a
form of exhaustive testing, Tatlock says.
This involves considering some component and showing every possible execution of steps up to some bound is correct.
“So I might make sure for the logging
system, there’s no execution within 100
steps that ever crashes. I get that by automatically testing every execution up to
100 steps.” Yet, he reiterates, the guarantee isn’t as strong, and bounded model
checking up to 100 steps does not tell you
anything about the 101st step.
Tatlock and his colleagues have built
a suite of tools the engineers use in their
regular development process. They include a checker that allows them to formally describe the entire radiotherapy
system to a computer and ensure the key
components are individually correct.
The researchers are now working on
building verified replacements for those
parts of the system. When all those individual system components are put
together, he says, essentially, they are assured top-level safety verification.
The radiotherapy system is checked
daily because “we want to make sure
the code written by the engineers on
that team will correctly turn off the
beam if anything goes wrong,” Tatlock says. The work is similar to DeepSpec’s; it just emphasizes a different
degree of automation.
While CertiKOS prevents one app
from incorrectly reading the memory
of another application, the UW team
does not use it because CertiKOS is
a traditional Unix OS meant for running Unix-style apps, and the preponderance of components in the
radiotherapy system are embedded
systems and just run code directly on
the hardware, he says.
Like Tatlock, Appel and Shao stress
that only certain types of critical soft-