Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation
The present and the previous article on Realistic Correct Systems Implementation together address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we want to ask: Can informaticians righteously be accounted for incorr...
Збережено в:
| Дата: | 2015 |
|---|---|
| Автори: | , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
PROBLEMS IN PROGRAMMING
2015
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/8 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-8 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/d2/5f28d63083ed7b8263ec021f400ed5d2.pdf |
| spelling |
pp_isofts_kiev_ua-article-82018-10-02T13:33:23Z Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation Cпособна ли информатика обосновывать построение больших компьютерных систем? Часть II. Доказательное построение компиляторов Чи здатна інформатика обґрунтовувати побудову великих комп’ютерних систем? Частина II. Доказова побудова компіляторів Goerigk, W. Langmaack, H. The present and the previous article on Realistic Correct Systems Implementation together address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we want to ask: Can informaticians righteously be accounted for incorrectness of ystems, will they be able to justify systems to work correctly as intended? We understand the word justification in this sense, i.e. for the design of computer based systems, the formulation of mathematical models of information flows, and the construction of controlling software to be such that the expected system effects, the absence of internal failures, and the robustness towards misuses and malicious external attacks are foreseeable as logical consequences of the models. Since more than 40 years, theoretical informatics, software engineering and compiler construction have made important contributions to correct specification and also to correct high-level implementation of compilers. But the third step, translation — bootstrapping — of high level compiler programs into host machine code by existing host ompilers, is as important. So far there are no realistic recipes to close this gap, although it is known for many years that trust in executable code can dangerously be compromised by Trojan Horses in compiler executables, even if they pass strongest tests. Our article will show how to close this low level gap. We demonstrate the method of rigorous syntactic a-posteriori code inspection, which has been developed by the research group Verifix funded by the Deutsche Forschungsgemeinschaft (DFG). Много лет теоретическая информатика в части разработки программного обеспечения и построения компиляторов занималась проблемами правильности спецификаций и высокоуровневых реализаций компиляторов. Во второй части статьи рассматривается проблема корректного и безопасного перевода (bootstrapping) программ с языка высокого уровня в коды машины. Показано, как решаются проблемы корректности программ на языках низкого уровня. Продемонстрирован метод строго синтаксического апостериорного анализа, который был разработан исследовательской группой Verifix в университете г. Киля (ФРГ). Багато років теоретична інформатика вчастині розробки програмного забезпечення і побудови компіляторів займалась проблемами правильності специфікацій і високорівневих реалізацій компіляторів. У другій частині статті розглядається проблема коректного і безпечного перекладу (bootstrapping) програм з мови високого рівня в коди машини. Показано, як вирішуються проблеми коректності програм на мовах низького рівня. Продемонстрований метод строго синтаксичного апостеріор ного аналізу, котрий був розроблений дослідною групою Verifix в університеті м. Киля (ФРН). PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2015-07-01 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/8 PROBLEMS IN PROGRAMMING; No 2 (2003) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2 (2003) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2 (2003) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/8/13 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2018-10-02T13:33:23Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
|
| spellingShingle |
Goerigk, W. Langmaack, H. Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| topic_facet |
|
| format |
Article |
| author |
Goerigk, W. Langmaack, H. |
| author_facet |
Goerigk, W. Langmaack, H. |
| author_sort |
Goerigk, W. |
| title |
Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_short |
Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_full |
Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_fullStr |
Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_full_unstemmed |
Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_sort |
will informatics be able to justify the construction of large computer based systems? part ii. trusted compiler implementation |
| title_alt |
Cпособна ли информатика обосновывать построение больших компьютерных систем? Часть II. Доказательное построение компиляторов Чи здатна інформатика обґрунтовувати побудову великих комп’ютерних систем? Частина II. Доказова побудова компіляторів |
| description |
The present and the previous article on Realistic Correct Systems Implementation together address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we want to ask: Can informaticians righteously be accounted for incorrectness of ystems, will they be able to justify systems to work correctly as intended? We understand the word justification in this sense, i.e. for the design of computer based systems, the formulation of mathematical models of information flows, and the construction of controlling software to be such that the expected system effects, the absence of internal failures, and the robustness towards misuses and malicious external attacks are foreseeable as logical consequences of the models. Since more than 40 years, theoretical informatics, software engineering and compiler construction have made important contributions to correct specification and also to correct high-level implementation of compilers. But the third step, translation — bootstrapping — of high level compiler programs into host machine code by existing host ompilers, is as important. So far there are no realistic recipes to close this gap, although it is known for many years that trust in executable code can dangerously be compromised by Trojan Horses in compiler executables, even if they pass strongest tests. Our article will show how to close this low level gap. We demonstrate the method of rigorous syntactic a-posteriori code inspection, which has been developed by the research group Verifix funded by the Deutsche Forschungsgemeinschaft (DFG). |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2015 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/8 |
| work_keys_str_mv |
AT goerigkw willinformaticsbeabletojustifytheconstructionoflargecomputerbasedsystemspartiitrustedcompilerimplementation AT langmaackh willinformaticsbeabletojustifytheconstructionoflargecomputerbasedsystemspartiitrustedcompilerimplementation AT goerigkw cposobnaliinformatikaobosnovyvatʹpostroeniebolʹšihkompʹûternyhsistemčastʹiidokazatelʹnoepostroeniekompilâtorov AT langmaackh cposobnaliinformatikaobosnovyvatʹpostroeniebolʹšihkompʹûternyhsistemčastʹiidokazatelʹnoepostroeniekompilâtorov AT goerigkw čizdatnaínformatikaobgruntovuvatipobudovuvelikihkompûternihsistemčastinaiidokazovapobudovakompílâtorív AT langmaackh čizdatnaínformatikaobgruntovuvatipobudovuvelikihkompûternihsistemčastinaiidokazovapobudovakompílâtorív |
| first_indexed |
2025-07-17T10:09:05Z |
| last_indexed |
2025-07-17T10:09:05Z |
| _version_ |
1850413018894041088 |
| fulltext |
Теоретические и методологические основы программирования
© Wolfgang Goerigk, Hans Langmaack, 2003
ISSN 1727-4907. Проблемы программирования. 2003. № 2 3
UDC 681.3.51
Wolfgang Goerigk, Hans Langmaack
WILL INFORMATICS BE ABLE TO JUSTIFY THE
CONSTRUCTION OF LARGE COMPUTER BASED SYSTEMS?
PART II. TRUSTED COMPILER IMPLEMENTATION1
The present and the previous article on Realistic Correct Systems Implementation to-
gether address correct construction and functioning of large computer based systems. In
view of so many annoying and dangerous system misbehaviors we want to ask: Can infor-
maticians righteously be accounted for incorrectness of systems, will they be able to justify
systems to work correctly as intended? We understand the word justification in this sense,
i.e. for the design of computer based systems, the formulation of mathematical models of
information flows, and the construction of controlling software to be such that the ex-
pected system effects, the absence of internal failures, and the robustness towards misuses
and malicious external attacks are foreseeable as logical consequences of the models.
Since more than 40 years, theoretical informatics, software engineering and compiler
construction have made important contributions to correct specification and also to correct
high-level implementation of compilers. But the third step, translation — bootstrapping —
of high level compiler programs into host machine code by existing host compilers, is as
important. So far there are no realistic recipes to close this gap, although it is known for
many years that trust in executable code can dangerously be compromised by Trojan
Horses in compiler executables, even if they pass strongest tests. Our article will show how
to close this low level gap. We demonstrate the method of rigorous syntactic a-posteriori
code inspection, which has been developed by the research group Verifix funded by the
Deutsche Forschungsgemeinschaft (DFG).
1Supported by Deutsche Forschungsgemeinschaft (DFG) under the grants La426/15 and /16.
1. Realistic Correct Systems
Implementation
As an introduction to the present
article, which focuses on trusted compiler
implementation, we want to summarize
and repeat some of the important defini-
tions from the previous article [Goe-
rigk/Langmaack01c] on Realistic Correct
Systems Implementation.
Compiler construction is crucial to
the construction of computer based sys-
tems, and correct realistic compilers are
necessary for a convincing construction
process of correct software/hardware sys-
tems. Correct realistic compilation is nec-
essary, can be achieved and it establishes
a trusted execution basis for further soft-
ware development. Most faults and bugs
are indeed found in software design and
high-level software engineering, however,
we find considerably many compiler bugs
as well [GccBugList], and one or the
other turns out to be critical. Unless the
implementation and integration gap of
software systems is closed with mathe-
matical rigor, the risk of incorrect code
generation will always seriously disturb
the recognition of and the trust in certain-
ties which are guaranteed by mature
software engineering and formal methods.
The rigid nature of matter educates
hardware technologists to be extremely
sensitive towards hardware failures; they
are felt as sensations. So system faults are
mostly and increasingly caused by soft-
ware. This observation is crucial. Software
engineers are permitted to assume hard-
ware to work correctly, and to exploit
this assumption for equally sensitive rig-
orous low level implementation verifica-
tion of software. We will demonstrate this
in a non-self-evident way in particular for
compilers, because they are crucial to
low level implementation correctness of
application software. At the upper end,
software engineers rely on the machine
independent semantics for their high-
level languages, but they have to be
aware of what kind of implementation
correctness makes sense and can realisti-
cally be guaranteed in their application
domain.
Теоретические и методологические основы программирования
4
Correct realistic compilation is the
major topic of the German joint project
Verifix on Correct Compilers of the uni-
versities of Karlsruhe, Kiel and Ulm [Go-
erigk97d, Goos/Zimmermann99]. The goal
is to develop repeatable engineering me-
thods for the construction and correct
implementation of compiler programs for
realistic, industrially applicable imperative
and object-oriented source programming
languages and real world target and host
processors, which generate efficient code
that compares to unverified compilers.
A number of key ideas and achie-
vements make this possible and help to
modularize the entire effort into suffi-
ciently small steps: an appropriate realis-
tic notion of correct implementation and
compiler correctness [Goerigk/Langma-
ack01c, Mueller-Olm/Wolf99], the reuse
of approved compiler architecture and
construction and compiler generator
techniques [Goos/Zimmermann99], the
method of a-posteriori program result
checking [Goerigk+98], mechanical proof
support [Dold+02], and finally, a trusted
initial compiler executable for a realistic
imperative high-level system programming
language [Goerigk/Hoffmann98b, Goe-
rigk/Hoffmann97]. The initial compiler
and in particular its low-level machine
implementation verification is the topic of
the present paper. The compiler serves as
a sound bootstrapping and implementa-
tion basis and lifts proof obligations from
machine code level to much more ab-
stract source code. It is proved to at most
generate correct implementations of well-
formed source programs; it may fail, e.g.
due to resource errors, and if the source
program is not well formed, then the tar-
get code may cause unacceptable errors
and compute unpredictable results. But if
the source program is well-formed, and if
the compiler succeeds, then the target
code is a correct implementation of the
source program. The compiler is imple-
mented and runs on a concrete physical
processor.
In the companion article [Goe-
rigk/Langmaack01c] on Realistic Correct
Systems Implementation we gave an ex-
tended motivation also for the impact of
the question raised in the title of the two
articles. Furthermore we modularized the
entire compiler verification effort in three
steps and developed a mathematical the-
ory which realistically and rigorously al-
lows to express compiling specification
correctness and high-level and low-level
compiler implementation correctness com-
positionally by commutative diagrams.
The present article focuses on the
realistic method for low-level compiler
implementation verification by bootstrap-
ping and syntactical a-posteriori code in-
spection, which we have developed in
order to provide, for the first time, a rig-
orously verified and fully trusted initial
compiler executable.
We want to summarize the impor-
tant definitions and observations from the
previous article [Goerigk/Langmaack01c].
We will repeat the definition of correct
implementation between source and tar-
get programs, and the modularization of
the entire proof effort in three steps. For
details, however, we want to refer to [Go-
erigk/Langmaack01c].
1.1. Compiling Specification and
Compiler Implementation. Compiling
(specification) verification involves se-
mantics. It is the first step necessary to
modularize the entire correctness proof.
The second step is correct compiler im-
plementation, i.e. the correct transforma-
tion of the compiling specification to ma-
chine code of the compiler host proces-
sor. Proving its correctness is called com-
piler implementation verification. Correct
compiler source programs are imple-
mented by bootstrapping. In practice we
can further modularize compiler imple-
mentation in high-level compiler imple-
mentation and low-level compiler ma-
chine implementation.
High-level compiler implementation
corresponds to programming. Likewise,
high-level compiler implementation veri-
fication is program verification. Machine
level compiler implementation correctness
can be established by a trusted initial
compiler, or by syntactical a-posteriori
result checking (as in Section 4).
Three tasks are necessary in order
to present a convincing correctness proof
Теоретические и методологические основы программирования
5
of a compiler executable on a compiler
host machine. SL and TL are abstract
source and target languages with conc-
rete representation domains indicated by
primes. HL is the compiler host language,
and HML is the compiler host machine
language. The compiler program τHL is
written in HL and compiled into executa-
ble code τHML written in HML. [[τHL]] HL and
[[τHML]] HML denote the respective semantical
relations. We will later simplify the situa-
tion and identify source and host lan-
guages as well as target and host machine
language. Using this notation, we can
modularize the problem in three tasks:
1. Specification of a compiling re-
lation C between SL and TL, and compil-
ing (specification) verification w.r.t. an
appropriate semantics relation between
language semantics [[٠]] SL, [[٠]] TL.
2. Implementation of a correspon-
ding compiler program τHL in HL, and
high level compiler implementation veri-
fication (w.r.t. C and to program repre-
sentations φSL
SL‘ and φTL
TL‘).
3. Implementation of a correspon-
ding compiler executable τHML in HML,
and low level compiler implementation
verification (with respect to [[τHL]] HL and
program representations φSL‘
SL‘‘ and φTL‘
TL‘‘ ).
The last two tasks establish imple-
mentation correctness relations between
compiling specification, compiler source
program and compiler executable. Every
task will be formalized by a correspond-
ing commutative diagram (Figure 1).
Fig 1. Three tasks for correct compiler specification and implementation
In Figure 1, A ⇀ B denotes the
domain of relations and A → B of (partial)
functions from A to B. The semantical
mappings [[٠]] SL and [[٠]] TL are functions
from source language SL resp. target
language TL to their semantical domains
SemSL and SemTL (i.e. the semantics of a
well-formed program is uniquely deter-
mined). Compiling specifications C typi-
cally allow for more than only one target
program, and also compiler program se-
mantics might be non-deterministic.
Data and program representations, which
map abstract programs to concrete pro-
gram representations and to their string
representations, are in general relations,
anyway.
1.2. Preservation of Relative Cor-
rectness. In this article we focus on com-
pilers and transformational programs and
formalize operational program semantics
by error strict relations f ⊆ Di × Do be-
tween input and output domains, which
are extended by individually associated
disjoint non-empty error sets Ω = A ⊎ U
of acceptable and unacceptable errors.
One particular error ⊥ models infinite
computations.
If fs is a source and ft a target pro-
gram semantics, and if ρi and ρo are data
representation relations (strongly error
strict in both directions), then we define ft
to be a correct implementation of fs relative
to ρi and ρo and associated error sets, iff
Теоретические и методологические основы программирования
6
( ρi ; ft ) (d) ⊆ ( fs ; ρo) (d) ∪ Ao
holds for all d ∈ Di
s with fs (d) ⊆ Do
s ∪ Ao
s.
This exactly captures the intuitive re-
quirements: d ∈ Di
s is called admissible, if
it does not cause an unacceptable error
outcome, i.e. if fs (d) ∩ Uo
s = ∅. Non-
admissible inputs may cause unpredict-
able or arbitrary results. But if d is admis-
sible, then we can trust in results com-
puted by target program semantics: Ei-
ther the result is correct (representation
of a corresponding source program out-
put) or the target program execution
aborts (observably) with an acceptable
(resource) error.
Fig 2. Correct Implementation
The symbol ⊑ denotes this refine-
ment relation, and '';'' denotes (diagram-
matic) relational composition. ρi ; ft ⊒ fs ; ρo
(or ft ⊒ fs for short) means that ft correctly
implements or refines or is better than fs.
Note that ⊑ depicts (basically) a relati-
onal inclusion in opposite direction. De-
tails can be found in [Goerigk/Langma-
ack01c]. Our definition is a relational ver-
sion of relative correctness preservation
[Mueller-Olm/Wolf99, Wolf00] and can
be understood as a deliberate generaliza-
tion of partial respectively total correct-
ness preservation. It is both horizontally
and vertically transitive (compositional).
1.3. Precise View at the Three
Steps. We have to refer to [Goerigk/Lan-
gmaack01c] for details, but we want to
repeat the diagram which precisely de-
fines the proof obligations necessary in
order to work through a complete com-
piler correctness proof. We will focus on
the lowest diagram of Figure 3 in this ar-
ticle, and it relates the compiler machine
executable semantically to the high-level
compiler implementation. They work se-
mantically on different input and output
data domains of HL and HML which are
related by program representation rela-
tions [Goerigk/Langmaack01c]. The dif-
ference is indicated by primes and dou-
ble-primes in Figure 3. We now know
precisely every conjecture we have to
prove in order to implement an SL to TL-
compiler correctly as an executable pro-
gram on a host processor HM.
Every data set, program set and
semantics space, every program seman-
tics, data representation, program repre-
sentation, semantics function, compiling
specification, compiler semantics and se-
mantics relation has to be appropriately
extended by unacceptable and acceptable
error elements. The commutative dia-
grams of Figure 2 and 3 precisely express
Fig 3. This diagram is again, but now precisely, illustrating the three steps for correct
compiler implementation as of Figure 1
Теоретические и методологические основы программирования
7
that C is a correct compiling specifica-
tion, and that τHL respectively τHML are
correct compiler programs.
Programs and their representations
have equal semantics. But we should ex-
plicitly note that in diagram 3 the com-
piler program τHML is not a representation
of τHL. These two programs have in gen-
eral different semantics, but the former is
a correct implementation of the latter.
1.4. T-Diagram Notation. McKee-
man's so-called T-diagrams allow to illus-
trate the effects of iterated compiler ap-
plications in an intuitive way. We use
them as shorthand notations for particu-
lar diagrams as of Figure 4.
Fig 4. The situation which we will abbreviate
by McKeeman's T-diagrams
Recall that ℂ is the natural correct
compiling specification from SL to TL.
Well-formed programs and their (syntac-
tical) φ-representations have equal se-
mantics, and τHL‘ ∈ φHL
HL‘(τHL) is a well-
formed HL'-program compiling syntactical
SL' programs to syntactical TL'-programs.
HL' is the domain of perhaps more con-
crete syntactical representations of HL-
programs. In this situation we use the T-
diagram (Figure 5)
Fig 5. McKeeman's T-diagram as a short-
hand for the above situation
as an abbreviation for the diagram in
Figure 4. However, we have to keep in
mind that the concrete situation is a bit
more involved, that the T-diagrams do
not explicitly express crucial differences
between various program representations.
We need to distinguish programs, pro-
gram semantics and (syntactical) program
representations in order to suffice re-
quirements from practice. We cannot put
practitioners short by elegant but too
nebulous idealizations.
2. Related Work on Compiler
Implementation Verification
An extended discussion of related
work in the field of compiler verification
has been presented in our previous arti-
cle [Goerigk/Langmaack01c]. Recall that
we find intensive work on steps 1 and 2,
i.e. on compiling specification and on
high level compiler implementation veri-
fication, although often under unrealistic
assumptions so that the results have to be
handled with care. Step 3, however, has
nearly totally been neglected so far. If the
phrase ''compiler verification'' is used,
then most of the authors mean step 1.
There is virtually no work on full com-
piler verification. Therefore, the ProCoS
project (1989—1995) has made a clear
distinction between compiling verification
(step 1) and compiler implementation veri-
fication (steps 2 and 3) [Langmaack97b].
Compiling verification is part of
theoretical informatics and program se-
mantics, and high level compiler imple-
mentation verification (step 2) is a field
within software engineering. However,
compiler implementation correctness then
further depends on existing correct initial
host compilers, which are not available
up to now. Hackers might have intruded
Trojan horses [Thompson84, Goerigk99b]
via unverified start up compilers (cf. the
introduction to the first article [Go-
erigk/Langmaack01c] and the following
Section 4). This in view, we are finally
left on human checkability of mechanical
proof protocols (a-posteriori-proof check-
ing) and initial compiler machine code.
Literature on low and machine
level compiler implementation verifica-
tion (step 3) is by far too sparse. There
are only demands by some researchers
like Ken Thompson [Thompson84],
L.M. Chirica and D.F. Martin [Chirica/
Теоретические и методологические основы программирования
8
Martin86] and J S. Moore [Moore88,
Moore96], no convincing realistic meth-
ods. Here is the most serious logical gap
in full compiler verification. Unfortu-
nately, a majority of software users and
engineers — as opposed to mathemati-
cians and hardware engineers — do not
feel logical gaps to be relevant unless
they have been confronted with a
counter-example. So we need
A. convincing realistic methods
for low level implementation verification
(step 3)
B. striking counter-examples (fail-
ures) in case only step 3 has been left out.
Let us first step into B and hence
go on with an initial discurs on the po-
tential risk of omitting the low level ma-
chine code verification step for compilers.
3. The Risk of Neglecting Machine Level
Verification
Ken Thompson, inventor of the op-
erating system Unix, stated in his Turing
Award Lecture ''Reflections on Trusting
Trust'' [Thompson84]:
''You can't trust code that you did not
totally create yourself. (Especially code
from companies that employ people
like me.) No amount of source-level
verification or scrutiny will protect you
from using untrusted code.''
He underpinned his statement by
sketching the construction of an execu-
table binary machine code version of a C-
compiler which was wrong, although his
version successfully passed N. Wirth's
strong compiler or bootstrap test
[Wirth77], which is well-known to be ex-
tremely hard to deceive, and although we
may even assume that the corresponding
C-version of his compiler has been verified.
Let us assume there exists a binary
version τ0 of a C-compiler running on a
machine M0, and a (different) C-compiler
τ1 written in C generating code for a ma-
chine M1. A two step bootstrapping proc-
ess of τ1 on M0 generates a version τ3 (of
τ1), which is now formulated in binary
M1-machine code. If we assume τ0 and τ1
correct, and the machine M0 to work cor-
rectly, then τ3 is correct as well [Lang-
maack97a, Goerigk96b, Hoffmann98b].
By a third bootstrapping step of τ1,
we may compile τ1 to a new M1-binary τ4
using the compiler τ3 on machine M1. If
we assume the machine M1 to work cor-
rectly as well, then τ4 and τ3 are identical
[Goerigk99a], at least if we assume every
involved program deterministic. The third
bootstrapping step (and checking identity
of τ3 and τ4) is N. Wirth's so called strong
compiler or bootstrap test. It is employed
for safety reasons, if at least one of the
four above correctness assumptions can-
not be guaranteed.
Fig 6. Wirth's strong compiler test. Note:
Even if M0 and M1 are the same machine, τ0
and τ2 need not necessarily generate identi-
cal code. τ0 and τ2 are two different compil-
ers. In general, we know nothing about τ0's
target code.
But let us come back to Ken
Thompson's scenario: He manipulated τ0,
constructed a malicious τ̄ 0 that finally
produced a wrong τ̄ 3, although he fol-
lowed the entire above bootstrapping
process and τ̄3 passed the strong com-
piler test. Although the compiler source
program τ1 remains correct (unchanged),
and even if the machines M0 and M1 work
correctly, τ̄3 incorrectly translates at least
one C-source program, in his case the
Unix login command. He has introduced
a Trojan Horse in τ0, which is a very hid-
den error hard to detect by tests. The
manipulation of τ0 can even be steered so
that τ̄3 generates incorrect target code
for exactly two C-source programs [Goe-
Теоретические и методологические основы программирования
9
rigk99b] — one of which must be the
compiler source program τ1 itself, be-
cause otherwise, due to the strong com-
piler test, τ̄3 would be correct.
In any case, the crucial insight is
that all this might happen even if τ1 is
verified on source level [Goerigk99b, Go-
erigk00b]. Moreover, if the user would
try to convince her/himself of correctness
by a test suite, as this is common practice
today, she/he would have to find at least
one of the two incorrectly compiled pro-
grams among those billions of (and theo-
retically infinitely many) test candidates.
We easily imagine that program
validation by test is heavily overcharged
in case of compilers if their generation
employs unverified auxiliary software,
like τ0 in our case. We should well real-
ize the security impact of all this. Virtu-
ally every realistic software generation
basically depends on running non-veri-
fied auxiliary software. Since computers
nowadays are usually connected to the
world wide net, the software is more or
less open to hacker attacks, and might
already have been manipulated from out-
side. Fighting security attacks causes
much harder problems than avoiding un-
intentional bugs (safety). Safety, in a
sense, relies on statistically distributed
bugs by constructors' mistakes or materi-
als' faults, whereas for security we have
to be aware of subversive intent.
Note that one possible procedure
in order to uncover the malicious Trojan
Horse is to perform the compiler boot-
strap and hence use the compiler itself as
a test case. But note: this test case would
have to be performed very carefully,
which means that we have to run the
generated compiler τ̄ 3, apply it to τ1 and
to compare the result τ4 with the ex-
pected verified result that is given as part
of the test suite. We doubt, that any ex-
isting compiler binary (like τ4) has ever
been verified in this sense yet. Actually,
this is one of the essential tasks of the
present paper.
Unless we verify τ3 to be a correct
implementation of (the verified) τ1, any of
the compiler executables τ0, τ2, τ3, τ4, any
further bootstrapped compiler implemen-
tation, and any source program compiled
by one of these programs might eventu-
ally cause disastrous, even catastrophic
effects. We think that this well serves as
a striking counter example.
4. Realistic Method for Low Level
Compiler Generation
The question we are going to an-
swer now is how we attack task A of step
3. A first idea might be to apply software
engineering philosophy as for high level
implementation verification, i.e. to step-
wise refine the high level implementation
down to executable binary machine code
HML using verified transformation rules.
Then, as in the 60´s, we would have de-
veloped the entire machine code written
compiler by hand, although nowadays
supported by using the computer as an
efficient typewriter and maybe for check-
ing correct application of the implemen-
tation rules. However, as we have seen
before (section 4), we ought to have
doubts trusting implementations of auto-
matic checking routines as long as there
are no trusted, i.e. correctly implemented
initial compiler executables available.
Even if trained in mathematical rigor, no
software scientist would ever manually
construct or, more importantly, certify, a
real world compiler executable in ma-
chine code.
Therefore, we follow a different
approach, the Verifix-idea, to generate
even initial compiler implementations by
an approved method, thereby incorporat-
ing the necessary verifications. We pur-
sue N. Wirth's idea to bootstrap the
compiler and add a sufficient variant of
the strong bootstrap test [Goerigk/Hoff-
mann98].
We identify source and high level
implementation language SL = HL and
take a proper sublanguage ComLisp [Go-
erigk/Hoffmann96] of ANSI-Common-
Lisp = SL+. We further identify target
and low level implementation language
TL = HML and take the binary machine
code of a concrete processor M, e.g.
DEC α or INMOS-Transputer-T400. An
existing ANSI-Common-Lisp system with
Теоретические и методологические основы программирования
10
compiler τ0 is running on a workstation M0
with machine code TL0 = HML0, so that
our initial two bootstrapping steps to-
gether are a cross-compilation to TL-code
using the workstation as host machine.
Fig 7. Steps 1 and 2 for an initial full correct
compiler implementation
According to step 1 and 2 (section
1.1) we develop a correct SL to TL-
compiling specification C and correctly
implement it as a compiler program τSL,
now in SL = HL itself.
High level syntactical programs in
SL' and TL' are SL-data, i.e. s-expression
sequences. Abstract syntactical programs
in SL and TL are associated to SL', TL' by
bijections φSL
SL‘ and φTL
TL‘. We formulate C
such that it will relate target programs
πTL to well-formed source programs πSL at
most, i.e. for which source semantics
[[πSL]] SL are defined. We construct τSL
such that, if applied to well-formed
source programs in SL', τSL, or more pre-
cisely [[τSL]] SL, executed on an imagined
SL-machine, will either terminate suc-
cessfully or abort with an acceptable er-
ror due to target machine resource ex-
haustion. τSL has a pre-condition that re-
stricts its inputs to representations of
well-formed source programs. That is to
say, τSL might not check for well formed-
ness; but then, [[τSL]] SL has to have an un-
acceptable error outcome, perhaps speci-
fied non-deterministically, if applied to
SL-data that do not represent well-formed
SL-programs (see the discussion on ℂ in
[Goerigk/Langmaack01c]).
We will also need a version τ''SL
which works on machine representations
of s-expressions, for instance on character
sequences (strings, cf. Figure 8), which
form a particular subset of all s-ex-
pression sequences. Then, φSL‘‘
SL‘‘ = φTL‘‘
TL‘‘
are the known string representations for
s-expressions, and their inverses are sin-
gle-valued functions (a string denotes at
most one s-expression sequence). Note:
τ''SL is to be a correct implementation of
τSL. The operator read-sequence (used in
τSL in order to read s-expression se-
quences) is programmed in τ''SL as a
function procedure which reads character
sequences (using operators read-char and
perhaps peek-char) and returns a list of s-
expressions. Analogously the output is
programmed using character output, i.e.
the operator write-char. τ''SL‘‘ denotes a
string version representing τ''SL, i.e. (τ''SL,
τ''SL‘‘) ∈ φSL
SL‘‘.
Fig 8. A correct compiler τ''SL mapping
character sequences in SL'' to character
sequences in TL''
Fig 9. Bootstrapping the initial compiler. A
sufficient variant of Wirth's strong compiler
test (a-posteriori-syntactical code inspection)
guarantees fully correct implementation
Let us now (unrealistically) assume
for a moment, that τ0, M0's (the work-
Теоретические и методологические основы программирования
11
station's) Lisp-compiler, has been cor-
rectly developed and correctly imple-
mented in TL0. Then a threefold boot-
strapping (Figure 9) of τSL (often of a
byte-sequence or string representation)
eventually generates τ̄ TL, provided that
the three compiler executions of τ0, τ2,
and τTL successfully terminate with regu-
lar outputs τ2, τTL, and τ̄ TL, respectively.
Since τSL and τ0 are assumed correct, and
whenever the data abstractions ρi
SL
TL
-1
,
ρo
SL
TL
-1
, ρi
SL +
TL0
-1
, and ρo
SL +
TL0
-1
are single-
valued functions, we have the following
bootstrapping theorem [Langmaack97a,
Goerigk99a, Goerigk00a]:
Theorem 4.1. (Bootstrapping theo-
rem) The compilers τ2, τTL, and τ̄ TL are
correct, even correctly implemented on
hardware processor M0 resp. M. They are
all correct refinements of C and τSL.
In our case ρi
SL
TL
-1
, ρi
SL +
TL0
-1
, ρo
SL
TL
-1
and ρo
SL +
TL0
-1
are single-valued functions;
actually, they are just the same as φSL‘‘
SL‘‘
-1
,
φSL‘‘+
SL‘‘+
-1
, φTL‘
TL‘‘
-1
, and φTL’ 0
TL ‘‘0
-1
, respectively.
We prove Theorem 4.1 by successive ap-
plication of a bootstrapping lemma: Let τ0
and τ1
1 be two correct compilers and let
us apply τ0 to τ1:
Fig 10. Bootstrapping an initial compiler im-
plementation τ2
What can we expect in case of a
successful compilation with a regular re-
sult τ2 respectively a representation τ2‘?
The T-diagrams represent two commuta-
tive diagrams (Figure 11 for τ0, and Fig-
ure 12 for τ1).
1 We use τ1 here instead of τSL, because the follow-
ing argument works for any correct compiler
source program.
Moreover, τ0 is correct, and the result
of applying τ0 to τ1‘ is the regular HL-datum
τ2‘ ∈ Do
HLΩ = TL´Ω. Thus, [[τ1‘]] SL‘ ⊑[[τ2‘]]
TL‘,which means ρi ; [[τ2‘]] TL‘ ⊒ [[τ1‘]] SL‘ ; ρo.
Fig 11. Extended view at Figure 10 (part 1
for τ0)
Fig 12. Extended view at Figure 10
(part 2 for τ1)
Hence, also the diagram in Figure 13 is
commutative and, thus, vertical composi-
tion of the diagrams in Figure 12 and in
Figure 13 finally yields the following
bootstrapping lemma:
Lemma 4.2. (Bootstrapping lemma)
If (ρi
-1 ; [[٠]] SL´) and (ρo
-1 ; [[٠]] TL´ ) are rea-
sonable semantics functions (e.g. if ρi
-1, ρo
-1
are partial functions like in our case us-
ing Lisp s-expression sequences), then
Di
TL and Do
TL may be conceived to be con-
cretizations
SL´´ and
TL´´ of the pro-
gramming languages
SL,
SL´ and
TL,
TL´, and in case of regular termination of
τ0´ applied to τ1´, [[τ2´]] TL‘ = [[τ2]] TL is a cor-
rect implementation of [[τ1‘]] SL‘ = [[τ1]] SL and
by vertical composition also of C (Figure
Теоретические и методологические основы программирования
12
12, perhaps different from ℂ). Thus, τ2‘
and τ2 are correct compiler programs with
the T-diagram shown in Figure 14.
Fig 14. If τ0 and τ1 are correct compilers, then
so is τ2
Let us start a minor detour and
come back to the discussion in the first
article [Goerigk/Langmaack01c]: The
proof of the bootstrapping lemma shows,
that the (compiler generating) compiler
τ0‘ needs not be a regularly terminating
program for all well-formed input pro-
grams in SL' in order to be useful. τ0‘, ap-
plied to a well-formed program πSL‘ in
SL', even to a well-formed compiler like
π1‘, might run into an acceptable error in
ATL‘ = Ao
HL, perhaps due to a resource
violation like a memory overflow.
If τ0‘ terminates regularly, however,
then the associated regular result τ2‘ in
TL' is again a well-formed and correct
SL
to
TL-compiler. In other words: Since we
cannot expect τ0‘ to yield regular results
for all (arbitrarily large) source program
representations, τ0‘ will in general be cor-
rect in the sense of preservation of rela-
tive (partial) program correctness, but not
in the sense of preservation of regular (to-
tal) correctness [Goerigk/Langmaack01c].
Thus, the expected error behaviors
of SL -programs and in particular of τ1
and hence also of τ2, on the one hand,
might be of quite a different nature than,
on the other hand, of SL and hence in
particular of τ0.
SL might even be a
process programming language such that
we expect
SL-programs and their imple-
mentations in
TL to be regularly (totally)
correct. If τ1 preserves regular (total) pro-
gram correctness, then so will τ2, i.e. the
result of applying τ0 to τ1 [Goerigk/Lang-
maack01c].
That is to say: A partial correctness
preserving compiler τ0 may well generate
a total correctness preserving compiler
executable τ2 from a corresponding total
correctness preserving compiler source
program τ1. We hence have just given the
proof, that there is no need for trusted
compilers to be correct in the sense of
preservation of total correctness. We do
not depend on a guarantee of well-defi-
nedness while bootstrapping compilers.
This ends our detour and we come
back in particular to the strong compiler
(bootstrapping) test. Since τSL, restricted
to well-formed SL-programs, is determi-
nistic, we also have the following strong
compiler test theorem (variants can also
be found in [Langmaack97a, Goerigk99a,
Goerigk00a]). Whereas the proof of the
bootstrapping theorem (4.1) is a simple
application of the bootstrapping lemma,
the proof of the strong compiler test
theorem requires a more explicit exploi-
tation of the bootstrapping lemma.
Theorem 4.3. (Strong compiler test
theorem) The compilers τTL and τ̄ TL are
equal.
Proof. Let τSL and τ0 play the roles
of τ1 and τ0 in the lemma. We take a rep-
resentation τSL´ of (the well-formed ab-
stract s-expression) τSL. τSL´ is also a rep-
Fig 13. Commutative diagram corresponding to [[τ1‘]] SL‘ ⊑ [[τ2‘]] TL‘
Теоретические и методологические основы программирования
13
resentation of the abstract SL+-program
τSL. SL and SL+ have the same input and
output data domains (of concrete s-
expression sequences). τSL and τSL´ have
the same semantics [[τSL]] SL = [[τSL]] SL+ =
= [[τSL´]] SL´ = [[τSL´]] SL+´.
Let τ2´ be the concrete result of
successfully applying τ0 to τSL´ on host
machine M0. Due to the proof of the
bootstrapping lemma we have the follow-
ing commutative diagram:
Recall that we introduced lan-
guages SL'' and TL'' as reasonable repre-
sentations of SL, SL' and of TL, TL'. SL
and SL' resp. TL and TL' are isomorphic,
and the inverses of ρi
SL +
TL0
and ρo
SL +
TL0
are
single valued functions.
Let τTL´´ be the concrete successful
result of compiling τSL´ by τ2´ again on
the host machine M0. Again, due to the
proof of the bootstrapping lemma we
have
Let τ̄ TL´´ be the concrete successful
result of compiling τSL´ by τTL´´, now on
machine M. Since τSL is assumed deter-
ministic (which actually can be guaran-
teed by construction), τTL´´ and τ̄ TL´´ are
representations of one and the same con-
crete s-expression sequence τTL´ = τ̄ TL´ in
Do
SL+ = Do
SL = TL' and of τTL = τ̄ TL in the ab-
stract language TL.
We can not prove equality of τTL´´
and τ̄ TL´´. Equality does in general not
hold, because the code of τTL´´ and of τ̄ TL´´
has been generated by two perhaps dif-
ferent code generation mechanisms of τ2ґ
on M0 resp. of τTL´´ on M, i.e. by two dif-
ferent compilers on two different ma-
chines. The code τTL´´ is influenced by
runtime-system code (in particular by
print-routines) which τ0, e.g. the existing
SL+ = ANSI-Common Lisp compiler run-
ning on M0, attaches as part of τ2´´ (which
generates τTL´´), whereas the code of τ̄ TL´´ is
influenced by runtime-system code which
our compiler executable (τ 2´) attaches as
part of τTL´´ (which generates τ̄ TL´´).
Let us for instance assume τTL´´ and
τ̄ TL´´ to be character sequence (string)
representations of τTL resp. τ̄ TL. Since
there are different correct string repre-
sentations of one and the same s-
expression, the M0-print routine of τ2´
might print τTL´´ differently to how τTL´´
prints τ̄ TL´´. But nevertheless, both are
correct printed representations of the
equal s-expressions τTL´ resp. τ̄ TL´.
However, we could add a further
bootstrapping step comparing the string
results of τTL and τ̄ TL. Since we would
then use the same print routines, and be-
cause our programs are deterministic, we
would finally get equal string representa-
Теоретические и методологические основы программирования
14
tions τ̄ TL´´ = ¯̄τ TL´´, if the bootstrap succeeds.
In order to see this, we exploit that τTL,
τTL´´, τ̄ TL, τ̄ TL´´ are semantically equal and
that their string representations represent
one and the same s-expression. Here is
another important remark: The loading
mechanism on machine M must not de-
pend on different binary (character se-
quence) representations τTL´´ resp. τ̄ TL´´ of
τTL = τ̄ TL. The loader has to load the same
abstract M-machine program in both
cases.
In any case, we could also start the
entire bootstrapping process by applying
τ0 on M0 to τ''SL´´. Recall that the latter is
a version of our compiler source program
τSL which does not use the standard op-
erators read and print of the runtime-
system of the implementing compiler to
read and print s-expressions, but com-
prises its own reading and printing rou-
tines (implemented by character in-
put/output-routines read-char, peek-char,
and write-char). Hence, it transforms
character sequences. In that case, both
programs are guaranteed to deterministi-
cally compute the same sequence of
characters, even on different machines.
Like in the proof of Theorem 4.3 we
could then show equality of the character
sequences τ''TL´´ = τ̄ ''TL´´, because their rep-
resentations by φTL‘
TL‘‘ are single-valued.
But note that this is again only
true if we compare the printed character
sequences. On binary level, they might
for instance be represented in different
character codings on M0 and M, say in
8bit-ASCII or in 16bit-Unicode.
Let us end this section with the fol-
lowing remark: We are well aware that
the previous observations are tedious,
cumbersome and by far not obvious. But
on the other hand, we have too often
seen compilers generating wrong code
just because they have been bootstrapped
or cross-compiled in a quick-and-dirty
process, forgetting about potential code
representation problems like for instance
byte order, alignment or even different
character codes used on different ma-
chines. Fortunately, our rigorous mathe-
matical treatment of code generation and
compiler bootstrapping enables to un-
cover any of these tedious problems and
to talk about them precisely.
5. Source Level Verification is not
Sufficient
Note, that all this has been proved
under the unrealistic assumption that τ0 is
correct. But there is no guarantee in the
situation we are aiming at: We want to
construct and generate an initial (first)
correctly implemented compiler executa-
ble. Nevertheless, we can use τ0 and τ2 as
intelligent (and efficient) tools, and they
will often succeed to produce the correct
result. We just have to assure this fact.
This is the key idea of our approach to
low level compiler implementation verifi-
cation.
However, the successful bootstrap
test (τTL = τ̄ TL) does not help. It is well-
known that it might succeed for incorrect
compiler source programs τSL. Just con-
sider a source language construct, which
is incorrectly compiled but not used in
the compiler itself.
Our situation is more delicate: τSL
is a verified compiler source program.
Unfortunately, we can prove [Goerigk99a,
Goerigk99b, Goerigk00b] even in this
case: Although τ̄ TL is successfully gener-
ated from the verified τSL by threefold
bootstrapping and passes the strong
compiler test, τTL is not necessarily cor-
rect. Ken Thompson's Trojan Horse,
originally hidden in τ0, might have sur-
vived so that we find it both in τTL and in
τ̄ TL (and also in τ2).
In [Goerigk99b, Goerigk00b], we
prove this fact mechanically using M. Ka-
ufmann's and J Moore's logic and theo-
rem prover ACL2 [Kaufmann/Moore94].
Ken Thompson's Trojan Horse can be ex-
pressed in high level language, even in
the clean and abstract Boyer/Moore-logic
of first order total recursive functions. We
need no ugly machine code to construct
such a malicious program part. The situa-
tion is even more delicate if we consider
preceeding or subsequent compilation
phases: If only one phase is corrupted,
the only chance to uncover that error is
Теоретические и методологические основы программирования
15
to rigorously check the target code of ex-
actly that phase, while the compiler ex-
ecutable τTL (or τ2) compiles τSL. No other
test will help, unless the user by accident
runs τTL on exactly that one additional
incorrectly compiled source program that
eventually causes catastrophic effects
(and waits for the catastrophe to happen).
6. Realistic Method for Low Level
Compiler Verification
Let us now drop our assumption
that τ0 is correct. Also note that, in gen-
eral, programs are non-deterministic. By
twofold bootstrapping of τ''SL resp. τ''SL´´
on machine M0 we generate an output
string s which is supposed to be a string
representation of τ''TL. This is according
to the first two steps of Figure 9. Since τ0
and hence τ2 might be incorrect, we have
to make sure with mathematical rigor,
that s is indeed a representation of τ''TL.
Our method of low level compiler
implementation verification is as follows:
Let τ''TL be a program written in TL such
that τ''SL C τ''TL holds, i.e. let τ''SL, τ''TL ful-
fill the compiling specification which was
verified in step 1 (Figure 7). Hence, τ''SL's
and τ''TL's semantics are related by ⊑.
Fig 15. Correct implementation of correct
compiler source programs. The extended se-
mantics, defined on Di
SL Ω resp. Di
TL Ω, carries
an unacceptable error outcome in Ui
SL resp.
Ui
TL indicating the cases where inputs do not
represent well-formed SL- or TL-programs
φSL‘‘
SL‘‘ , φ
TL‘‘
TL‘‘ are the natural 1-1-
mappings on character sequences. How
ρi
SL
TL, ρo
SL
TL are precisely defined depends
on which primitive standard input-output-
routines are actually used in SL and TL.
Since ρi
SL
TL
-1 = ρo
SL
TL
-1 is single-va-
lued, representations of well-formed pro-
grams have unique semantics in Sem SL
resp. Sem TL. Due to vertical composability
(cf. [Goerigk/Langmaack01c]), τ''TL is a
correct SL'' to TL''- compiler correctly
implemented in TL. Figure 15 accom-
plishes Figure 7 and 8 and yields Figure 1
in our special situation.
Any of our data including pro-
grams are representable by s-expressions.
Thus, we may assume that any of our
source and target languages L have
s-expression-syntaxes, i.e. syntactical pro-
grams are s-expression sequences. Input
and output data domains Di
L, Do
L are sets
of s-expression sequences as well. Note
that characters are particular s-expressi-
ons, and hence character sequences
(strings) are particular s-expression sequ-
ences. Not every syntactical program (s-
expression) is well-formed. In fact, the set
of well-formed programs is exactly the
domain of definition of the semantics
function [[٠]] L ∈ Sem L.
Compiling specifications C are of-
ten defined by syntactical rules (e.g. by
term rewriting), whereas correctness of
τ''TL is a semantical matter. That is to say:
We have a reduction of the correctness
problem from semantics to syntax. The
previous paragraphs sketch the proof of
the following theorem:
Theorem 4.4. (Semantics to Syntax
Reduction) If s is a string, if τ''TL =
= (φTL
TL‘‘ ; φ
TL‘‘
TL‘‘)
-1(s) and if syntactical che-
cking of τ''SL C τ''TL is successful, then τ''TL
is a well-formed SL'' to TL'' compiler cor-
rectly implemented in TL.
It is not in all cases necessary to
completely verify an algorithm before-
hand in order to trust a computed result.
In the proposed process for correct com-
piler construction, we verify τSL resp. τ''SL
a-priori (steps 1 and 2), but verification of
τTL resp. τ''TL (step 3) is an a-posteriori
syntactical result checking. It allows for
using unverified supporting software, e.g.
compilers τ0 and τ2 on machine M0. They
are used as intelligent but not necessarily
correct type writers. Checking guarantees
to find any error in τ''TL, even intended
errors like viruses or Trojan horses as of
section 4.
Теоретические и методологические основы программирования
16
The idea of a-posteriori result
checking is old. We can find applications
e.g. in high school mathematics, like
checking division or linear equation solv-
ing by (matrix-vector) multiplication. The
idea has found its way to algorithms the-
ory [Blum+89], trusted compilation [Lang-
maack97b, Langmaack97c, Goerigk/Hoff-
mann98, Pnueli+98, Heberle+98, Gaul-
+99, Cimatti+97], and systems verifica-
tion [Goerigk+98, Bartsch/Goerigk00d]
in general.
6.1. Realistic Syntactical a-poste-
riori Code Inspection. However, since we
know that realistic compiling specifica-
tions and compilers are of tangible size,
we might ask if syntactical a-posteriori
code checking is realistically manage-
able. A first idea might be to look for
machine support, i.e. to write checking
algorithms and programs. But we should
be aware that in this way we might well
run into circulos vitiosos. We burden our-
selves with new specification and (high
and machine level) implementation cor-
rectness problems for checking algo-
rithms and programs. If we want to im-
plement an initial compiler fully correctly
on a machine, there is no way around
some hand checking.
Remark: We do not condemn the
use of programmed computers for proving
and proof checking. If a software engineer
believes in auxiliary software to be suffi-
ciently trustful, she or he is allowed to use
it in order to gain more reliable software
production. However, the software engi-
neer should then make clear which parts
of the auxiliary software he/she has used
and hence relies on although still not be-
ing rigorously verified modulo hardware
correctness. We have shown techniques
how to maliciously harm auxiliary soft-
ware. It is most important for the IT-
community to demonstrate sound and re-
alistic means how to stop such ever last-
ing circulos vitiosos. Since source code
verification may succeed, and since man-
ual machine code verification hardly ever
will do, we strongly believe that providing
trustworthy compiler executables is the
most promising sound basis.
Verifix has introduced [Goerigk/
Hoffmann98, Hoffmann98b] three inter-
mediate languages between SL (Com-
Lisp) and TL (INMOS Transputer- or
DEC α-code). Because it is necessary to
finally produce a convincing complete
rigorous proof document, these lan-
guages have particularly been chosen in
order to isolate crucial compilation steps
and to enable code inspection by target
to source code comparison. Essential
characteristics and advantages for code
inspection are:
• Languages Li are close to their
preceeding languages Li-1 so that only
few crucial translation steps are necessary
per pass.
• Translation uses standard tech-
niques, does only moderately expand and
is local in the sense that it does not reor-
der corresponding thick code pieces.
• We avoid optimization; every
transition remains well recognizable and
locally checkable w.r.t. CLi
Li+1 by juxta-
posing corresponding code.
• Every language has a procedure
or subroutine concept; source and target
programs are modularized by correspond-
ing subroutines.
These characteristics will be re-
flected by our checking (i.e. compiling
specification and code inspection) rules
in section 6.2 below. Source, intermediate
and target languages are:
1. High level source language is
ComLisp = SL. Programs consist of non-
nested mutually recursive function pro-
cedures with call-by-value parameter
passing. Variables are simple, and data
are Lisp-s-expressions. Denotational, op-
erational copy rule resp. stack semantics
are well-known [Loeckx/Sieber87, Niel-
son/Nielson92].
2. Stack Intermediate Language
SIL. Programs consist of non-nested mu-
tually recursive parameterless procedures.
Data remain s-expressions. Operators are
postfixed (reverse Polish notation), paren-
theses are dropped, and variables are
represented by frame-pointer based stack
locations (usually very small relative ad-
dresses) intended to implement proce-
Теоретические и методологические основы программирования
17
dure and operator parameters. Opera-
tional stack semantics is straight forward
and easily comparable to the operational
SL-semantics.
3. C-like intermediate language
Cint similar to Java's virtual machine lan-
guage. All variables are of type integer,
contents are either immediate or referen-
ces into two linear stack resp. heap ar-
rays. The stack is intended to implement
SIL's stack, and the heap to refine non-
atomic Lisp-s-expressions (SIL-data). Every
SIL-program can be implemented in Cint
with equivalent semantics.
4. Assembly language TA. Instruc-
tions are machine dependent, e.g. Trans-
puter or DEC α. Symbolic addresses are
avoided; subroutines are called using
unique numbers, variables have small
relative addresses, branches stay within
subroutine bodies and are instruction
counter relative.
5. Machine code TL. Binary or
hexadecimal notation of byte contents
with more or less implicit prescription of
how to load registers and memory of the
target machine. The implicit prescription
is materialized by a small boot program
[Goerigk/Hoffmann97]. Only TA and TL
are machine dependent.
Semantics of a TL-program πTL is
given by execution of the machine M,
after the instruction counter has been
loaded with the start address of the main
part of πTL. Memory cells and registers
not explicitly mentioned in the loading
process are assumed to contain arbitrary
data, i.e. πTL might behave non-deter-
ministically, although each instruction
works deterministically. πTL might in ge-
neral even overwrite itself. However, the
programs we generate will not. In case
we prove preservation of partial correct-
ness, they will instead stop with an error
message like ''stack overflow'', ''heap
overflow'', ''return stack overflow'' or
''arithmetic overflow'', or due to operator
undefinedness. This is guaranteed by com-
piling specification verification (step 1).
6.2. A Closer Look into a-posteriori
Code Inspection. In the following we re-
fer to our concrete compiler implementa-
tion from SL = ComLisp to binary Tran-
sputer machine code TL [Goerigk/Hoff-
mann98, Goerigk/Hoffmann97, Goerigk/
Hoffmann98b]. The compiler proceeds in
four separate phases. Each phase is cor-
rectly implemented in ComLisp and gen-
erates an external string representation of
the intermediate and target programs.
Checking the entire transformation
of a Lisp-program directly into binary
Transputer-machine code is unrealistic.
We would have to check, that the hexa-
decimal representation of the code for
e.g. a function definition like
(DEFUN f (x y) (+ (* x y) 3))
which compiles into the Transputer-
machine code
(33 z 4a
75 e0 73 75 e1 73 fa d3 75 52 d5 75 74 f9 a2 21 f0 73 58 71
f9 a2 21 f0 73 30 73 e4 73 31 73 e5 73 32 73 e6 73 33 73 e7
44 70 21 3e f6 43 73 e6 43 73 e7 44 70 21 3c f6 73 34 73 e0
73 35 73 e1 75 60 5e d5 75 31 d3 75 30 f6)
is a correct one. Without any further
structure of the target code we would not
be able to do this conscientiously. The
vertical decomposition into intermediate
languages gives the necessary structure.
We will show this using the concrete
output of our compiler implementation
for the above function. It has no higher
control structures (no loops nor condi-
tionals). This slightly simplifies the pres-
entation here because we will not have to
check relative jump distances for the as-
sembly code.
6.2.1. Checking the Front End.
The first two compilation steps are ma-
chine independent. We start with our
original ComLisp-function and compile it
to SIL. This essentially is the transfor-
Теоретические и методологические основы программирования
18
mation of expressions into postfix form.
The body is compiled to (x y * 3 +),
augmented by relative positions of vari-
ables and intermediate results. The last
statement copies the result to the result
stack position 0.
(DEFUN f (x y) (DEFUN F
(+
(*
x (_COPY 0 2)
y (_COPY 1 3)
) (* 2)
3 (_COPYC 3 3)
) (+ 2)
) (_COPY 2 0))
Let us cite the compiling specifica-
tion rules which are necessary to check
that this particular source to target code
transformation has been computed ac-
cording to the specification. Note that
the software engineer does not even have
to understand the code semantically in
order to check this step1. The purely syn-
tactical (but semantically verified) com-
piling specification defines checking
rules. An average educated software en-
gineer will not be overtaxed and can
obey them in an informal but neverthe-
less clear, succinct and rigorous mathe-
matical proof style.
1. CLdef [[ (DEFUN p ( p 1 ... p k ) f 1 ... f m )]] γ ⊇def
⊇def (DEFUN p
CLprogn [[ f 1 ... f m ]] ρ, γ, k
(_COPY k 0))
where ρ( p i ) = i-1 for each i = 1, ..., k
2. CLprogn [[ f 1 ... f m ]] ρ, γ, k ⊇def CLform [[ f 1 ]] ρ, γ, k
...
CLform [[ f m ]] ρ, γ, k
where m ≥ 1
3. CLform[[(p f 1 ... f n )]] ρ, γ, k ⊇def CLform [[ f 1 ]] ρ, γ, k
...
CLform [[ f n ]] ρ, γ, k+n-1
(p k)
4. CLform [[c ]] ρ, γ, k ⊇def (_COPYC c k)
where c is a constant integer, charac-
ter, string or symbol NIL or T
1 Nevertheless, we will sometimes give comments
on the semantics in order to make this presenta-
tion more intuitive and readable.
5. CLform [[v ]] ρ, γ, k ⊇def (_COPY ρ(v) k)
where v is a local variable or formal
parameter with ρ(v) a defined natural
number
We present the compiling specifi-
cation rules in the style of a conditional
term rewrite system (for details see [Goe-
rigk/Hoffmann97, Hoffmann98b]). Ground
terms are s-expressions or s-expression
sequences from the syntactical domains
of source and target language, i.e. of
ComLisp and SIL: <program>, <decla-
rations>, <form>, <fname>, <ident>,
<operator>, <symbol>, <integer>, <cha-
racter>, <string> resp. <program>SIL,
<declarations>SIL, <form>SIL. Ground
terms are augmented by rewrite vari-
ables2 and unary rewrite operators like
CLdef [[٠]], CLprogn [[٠]] or CLform [[٠]] with pa-
rameters ρ, γ, k. Actually, ρ contains rela-
tive addresses for local variables and pa-
rameters, γ maps global variables to ''ab-
solute'' addresses, and k is the relative
result position corresponding to the
structural depth of source expressions.
We just presented those specification
rules necessary for our example.
The system of all conditional term
rewrite rules together defines multivalued
(non-deterministic) operations associated
to each rewrite operator, and we under-
stand the single rules above to specify
that the left hand side ground term set
contains the right hand side set of
ground terms by definition (⊇def). This is
an inclusion by definition, because there
might be other rules which apply to the
same left hand side pattern.
The simple structure of these rules
guarantees a simple checking process
because of their compositionality, order
preservation, at most linear expansion
and because rewrite operator applications
are not nested and procedure boundaries
are preserved.
2 We use the prefix rewrite in order to distinguish
rewrite variables from those ranging over program
fragments and rewrite operators from program
operators.
Теоретические и методологические основы программирования
19
The next step is data refinement of
dynamically typed Lisp-data to a linear
memory architecture. Relative addresses
are multiplied by 2 (tag and value field)
and copied in pairs. We have to focus on
single SIL statements and compare them
with pairs of target statements: In order to
copy the content of x from relative position
0 to 2, the target code has to copy the tag
field from 0 to 4 and the value field from 1
to 5. Operator calls now become subrou-
tine calls into the runtime system – com-
piling specification verification proves that
the runtime system procedures are correct
operation refinements of the SIL-operators.
(DEFUN F (DEFUN F (8)
(_COPY 0 2) (_SETLOCAL (_LOCAL 0) 4)
(_SETLOCAL (_LOCAL 1) 5)
(_COPY 1 3) (_SETLOCAL (_LOCAL 2) 6)
(_SETLOCAL (_LOCAL 3) 7)
(* 2) (* 4)
(_COPYC 3 3) (_SETLOCAL 3 6)
(_SETLOCAL 3 7)
(+ 2) (+ 4)
(_COPY 2 0)) (_SETLOCAL (_LOCAL 4) 0)
(_SETLOCAL (_LOCAL 5) 1))
Again, we cite the corresponding
conditional term rewrite rules from the
compiling specification from SIL to Cint
(ξ is a compiletime environment mapping
program constants such as symbols,
strings, and lists to linear heap represen-
tations and addresses):
1. CSdef [[(DEFUN p f 1 ... f m )]] ξ ⊇def
⊇def (DEFUN p (s)
CSform [[ f 1 ]] ξ
...
CSform [[ f m ]] ξ )
where s is the maximal stack frame
length needed by f1, . . . ,fm
2. CSform [[(_COPY i j)]] ξ ⊇def
⊇def (_SETLOCAL (_LOCAL 2i) 2j)
(_SETLOCAL (_LOCAL 2i+1) 2j+1)
3. CSform [[( p i )]] ξ ⊇def (p 2i)
4. CSform [[(_COPYC n i)]] ξ ⊇def
⊇def (_SETLOCAL τ 2i)
(_SETLOCAL n 2i+1)
where τ is the number tag 3 and n is
an integer
This completes checking the ma-
chine independent front end. The next two
steps are machine dependent. The final
step generates the machine code above.
6.2.2. Checking the Back End.
The first back end phase transforms con-
trol structure into linear assembly code
with relative jumps. The generated sub-
routine body consists of procedure entry
code, the main part and procedure exit
code, three parts which are structured in
three lists in the TA-code. Entry and exit
code share the same pattern for every
procedure. This phase also handles re-
source restrictions of the concrete 32-bit
machine. But this is a semantical issue
not to be checked here.
In order to check the main part, we
have to compare single Cint-instructions with
small groups of up to four or five assembly
instructions. For instance, the instruction
(SETLOCAL (LOCAL 0) 4) (the second
line in the Cint-definition) is compiled to the
instruction sequence LDL 3 LDNL 0 LDL
3 STNL 4 (first line of the TA-main part
below). It first loads the frame pointer, then
the content of relative position 0, which af-
ter loading the frame pointer again is finally
stored into relative position 4.
(DEFUN F (8) (_DEFCODE F 51
(LDL 5 STNL 0 LDL 3 LDL 5
STNL 1 LDL 3 OPR 10 STL 3
LDL 5 LDNLP 2 STL 5 LDL 5
LDL 4 OPR 9 CJ 2 OPR 16 LDL 3
LDNLP 8 LDL 1 OPR 9 CJ 2
OPR 16)
(_SETLOCAL (_LOCAL 0) 4) (LDL 3 LDNL 0 LDL 3 STNL 4
(_SETLOCAL (_LOCAL 1) 5) LDL 3 LDNL 1 LDL 3 STNL 5
(_SETLOCAL (_LOCAL 2) 6) LDL 3 LDNL 2 LDL 3 STNL 6
(_SETLOCAL (_LOCAL 3) 7) LDL 3 LDNL 3 LDL 3 STNL 7
Теоретические и методологические основы программирования
20
(* 4) LDC 4 LDL 0 LDNL 30 OPR 6
(_SETLOCAL 3 6) LDC 3 LDL 3 STNL 6
(_SETLOCAL 3 7) LDC 3 LDL 3 STNL 7
(+ 4) LDC 4 LDL 0 LDNL 28 OPR 6
(_SETLOCAL (_LOCAL 4) 0) LDL 3 LDNL 4 LDL 3 STNL 0
(_SETLOCAL (_LOCAL 5) 1) LDL 3 LDNL 5 LDL 3 STNL 1)
(LDL 5 LDNLP -2 STL 5 LDL 5
LDNL 1 STL 3 LDL 5 LDNL 0
) OPR 6))
The involved rules of the compil-
ing specification1 from Cint to TA are the
following:
1. CCdef [[(DEFUN f (σ)s 1 ... s n )]] ϕ ⊇def
⊇def (DEFCODE f ψ ( f )
(entrycode (σ))
(CCstmt [[s 1]] ϕ ,σ
...
CCstmt [[ s n ]] ϕ ,σ)
(exitcode)
where ϕ = <ψ, | stack |, | heap |> and ψ is
a subroutine numbering
2. CCstmt [[( f i)]] ϕ ,σ ⊇def
⊇def LDC i LDL start LDNL ψ ( f ) OPR 6
where 0 ≤ i < σ
3. CCstmt [[(_SETLOCAL e i )]] ϕ ,σ ⊇def
⊇def CCexpr [[e]] ϕ ,σ LDL base STNL i
where 0 ≤ i < σ
4. CCstmt [[(_LOCAL i)]] ϕ ,σ ⊇def
⊇def LDL base LDNL i
where 0 ≤ i < σ
In the first rule, σ is the stack
frame length of f, and we used σ (see
also the above code) to stress that the
procedure entry code is nearly constant,
i.e. only parameterized by the number σ.
|stack| and |heap| denote the initial stack
and heap size. In the second rule, i is the
relative address of the return value posi-
tion, start contains the jump table start
address, ψ(f) denotes the (constant) jump
table position of f 's start address, and
OPR 6 is the GCALL operation, i.e. the
subroutine jump. In the third and fourth
rule, base contains the ''absolute'' stack
frame base address and i is the relative
address of the variable to be assigned to
respectively loaded from.
Finally, it is easy to check that the
TA-mnemonics and decimal operands
have been transformed correctly to in-
struction byte sequences (cf. Figure 16).
Note, that in order to understand the
code semantically, we additionally would
have to know the semantics for instance
of the Transputer-operations called by
OPR instructions. We need not know this
information to perform syntactical check-
ing; the correctness of the code follows
from compiling verification, whereas we
have to check the code for compliance
with the specification. The TL-module
number #x33 = 51 below is a code
module (indicated by the character z)
that has a length of #x4a = 74 bytes.
(_DEFCODE F 51 (33 z 4a
(LDL 5 STNL 0 LDL 3 LDL 5 75 e0 73 75
STNL 1 LDL 3 OPR 10 STL 3 e1 73 fa d3
LDL 5 LDNLP 2 STL 5 LDL 5 75 52 d5 75
LDL 4 OPR 9 CJ 2 OPR 16 LDL 3 74 f9 a2 21 f0 73
LDNLP 8 LDL 1 OPR 9 CJ 2 58 71 f9 a2
1 The mechanical correctness proof of the corre-
sponding compiling specification [Dold+02] us-
ing the PVS theorem prover unvealed a tedious
bug in the procedure initialization code. Although
easy to repair, we prefer to leave the bug in the
code and make this remark instead. The OPR 10
(WSUB, word subscript) in the third line of the
code above is an address calculation which in-
deed does not check for overflow. Finding this
bug is due to the mechanized compiling verifica-
tion by using incorruptible and inexhaustible
theorem prover support. Since it is a relative ad-
dress calculation, it would hardly show up in any
practical test run.
Теоретические и методологические основы программирования
21
OPR 16) 21 f0
(LDL 3 LDNL 0 LDL 3 STNL 4 73 30 73 e4
LDL 3 LDNL 1 LDL 3 STNL 5 73 31 73 e5
LDL 3 LDNL 2 LDL 3 STNL 6 73 32 73 e6
LDL 3 LDNL 3 LDL 3 STNL 7 73 33 73 e7
LDC 4 LDL 0 LDNL 30 OPR 6 44 70 21 3e f6
LDC 3 LDL 3 STNL 6 43 73 e6
LDC 3 LDL 3 STNL 7 43 73 e7
LDC 4 LDL 0 LDNL 28 OPR 6 44 70 21 3c f6
LDL 3 LDNL 4 LDL 3 STNL 0 73 34 73 e0
LDL 3 LDNL 5 LDL 3 STNL 1) 73 35 73 e1
(LDL 5 LDNLP -2 STL 5 LDL 5 75 60 5e d5 75
LDNL 1 STL 3 LDL 5 LDNL 0 31 d3 75 30
OPR 6))) f6)
The involved compiling rules from
TA to TL are:
1. CAdef [[(DEFCODE f i b )]] ⊇def
⊇def (i#x z |c|#x c)
where c = CAbody [[b]] and i#x, |c|#x de-
note hexadecimal representations of
i,|c|
2. CAbody [[ op 1 e 1 ...( ...) ...( ... op n e n ) ]] ⊇def
⊇def CAopr [[ op 1 e 1 ]] ... CAopr [[ op n e n ]]
3. CAopr [[ op e ]] ⊇def prefix(assembleop(op, e)
In the second rule, CAbody ignores
the list (parentheses) structure, and in the
third rule we apply two auxiliary func-
tions: assembleop translates the 16 basic
transputer instruction mnemonics to
hexadecimal digits '0' up to 'f' according
to the table in Figure 16, and prefix gen-
erates the pfix/nfix-chains necessary
to load the value of e, which is in particu-
lar very easy for small non-negative
numbers between 0 and 15 (representable
by a four bit nibble).
That is to say: In order to check
the final code generation step, we only
need to know the 16 instruction mne-
monics, their mapping to instruction
code nibbles, and the pfix/nfix-chains
necessary to load large operands. So for
instance LDC 4 is transformed to 44
which loads the constant 4 into Areg,
whereas LDNL 28 is compiled into the
pfix-chain 21 3c, which will execute
LDNL on 16 × 1 + 12 = 28.
6.2.3. The Complete Proof Struc-
ture. This ends the more detailed look
into the characteristics of our technique
Fig 16. Transputer-architecture and direct function codes. The Transputer state consists of
the registers Areg, Breg, and Creg, which form a mini stack with top Areg, the operand reg-
ister Oreg, the instruction pointer (program counter) Iptr, the workspace pointer Wptr, vari-
ous flags like the ErrorFlag, some more registers and the memory Mem. The registers con-
tain Word valued quantities. The memory is byte or word addressable
Теоретические и методологические основы программирования
22
of a-posteriori code inspection by com-
paring corresponding code parts of the
respective source and target programs
and checking them to be in conformance
with the compiling specification rules.
In order to come back to the over-
all proof structure, note that program
fragments like those of the previous sec-
tion have been generated for the entire
compiler using four unsafe initial com-
piler implementations produced by τ0 on
machine M0 for both front-end and both
back-end phases.
The following large diagram (Fig-
ure 17) shows all four sub-compiling
specifications CLi-1
Li, all four hand-written
sub-compiler implementations τ''i,SL = τ''i,L1
and all 16 = 4 × 4 sub-compilers τ''i,Lj
generated and printed out by bootstrap-
ping. The specifications are verified by
compiling verification (step 1), the τ''i,SL
by high level implementation verification
(step 2) and the τ''i,Lj for j > 1 by low level
implementation verification (step 3), ac-
tually by checking
τ''i,Lj-1 CLj-1
Lj τ''i,Lj
which is exactly what we sketched in the
previous section and which we proved to
be sufficient due to the semantics to syn-
tax reduction Theorem 4.4.
However, it is not necessary to per-
form all those cumbersome checkings.
In particular, unpleasant low level ma-
chine) code inspections below the diago-
nal are redundant: Since CTA
TL and τ''4,SL
are correct (steps 1 and 2), and since
τ''4,TL is checked to be correctly compiled
to TL, τ''4,TL is a fully correct TA to TL-
compiler executable. We can use it to
correctly compile τ''3,TA to a correct τ'''3,TL,
which guarantees τ'''3,TL to be a fully cor-
rect Cint to TA-compiler executable, and
so forth.
That is to say: We load the correct
compiler τ''4,TL (actually τ''4,TL´´) into ma-
chine M using the boot program. Cor-
rectness of that program means and
hence guarantees that it follows the ex-
plicit and implicit loading prescriptions
of τ''4,TL´´. Then we start the loaded com-
piler in M and let M read τ''3,TA´´. If M
terminates successfully (regularly), then
due to Bootstrapping Theorem 4.1 the
output is a correct compiler τ'''3,TL (actu-
ally τ'''3,TL´´) as well, not necessarily iden-
tical to τ''3,TL, but according to CTA
TL.
We can now concatenate τ'''3,TL ;
τ''4,TL (actually τ'''3,TL´´ ; τ''4,TL´´) and obtain a
correct compiler executable from Cint'' to
TL'' due to composability of commutative
diagrams (cf. [Goerigk/Langmaack01c]).
If we proceed, this process will finally
generate the desired correct compiler ex-
ecutable from SL'' to TL''.
Fig 17. Special bootstrapping with four compiler phases. ϕ'' L =def (ϕ L
L´ ; ϕ L´
L´´)
Теоретические и методологические основы программирования
23
τ'''3,TL´´ = τ'''1,TL´´ ; τ'''2,TL´´ ; τ'''3,TL´´ ; τ''4,TL´´
Here we exploit Verifix's hardware
correctness assumption for verified low
level compiler implementation (step 3).
Note that we have implicitly introduced a
(syntactical) concatenation operator '';''
for sequential programs, which corre-
sponds to particular sequential composi-
tion. Its semantics is obvious. Any of our
languages allows for the syntactical con-
catenation of programs.
The compilers τ''i,SL contain a
parser for s-expression sequences, namely
the implementation of read-sequence. It
is part of the runtime system, and so far,
it has to be checked down to the diago-
nal, in particular and unfortunately also
as part of τ''4,TL resp. τ''3,TA in machine
code. However, there is a remarkable
chance to reduce the a-posteriori code
inspection work load considerably: Since
the print-routines are checked down to
machine code TL as well, we may in
principle check the (considerably larger)
read-routines by (trusted) printing of
their results, i.e. we may look at the
parser read-sequence as an additional ini-
tial compiler phase τ''0,SL. Then we only
need its correct implementation as a high
level SL-program and no further low level
implementation verification. In that case,
however, unchecked code runs initially,
and we need further precaution1, namely
to validate the intermediate machine
state after running the code of read-
sequence. We can exploit the processor's
memory protection mechanism and add a
few validations (runtime-checkings) to
sufficiently guarantee the relevant part of
the intermediate state not to be cor-
rupted. In later work we shall report on
this and give the necessary proofs.
7. Conclusions
At the end of our exposй we would
like to answer the question raised in the
title of this essay: Will informatics be
able to justify the construction of large
computer based systems? We will trace
1 Unfortunately, it seems again not to be sufficient
to compare the initially loaded and the generated
code to be identical (cf. section 4).
again the main lines of thought which
finally lead us to a rather confident an-
swer: Yes. In fact, internal misbehaviors
and intended external violations of com-
puter based systems need not last for-
ever, i.e. safety and security might re-
cover. However, this will not work out
unless software production and informat-
ics science carefully enough solve the
following problem: At the end it is the
executable binary real world processor
code, and not only high level specifica-
tions and programs, which has to be
guaranteed to behave correctly as re-
quired.
Realistic software production em-
ploys and relies on compilers for high
level languages, like for instance C,
C++, Ada, Java or Common Lisp. C is
very close to machine level, but in our
context it must be seen as a high level
language with very critical and decisive
compilation steps towards real processor
code.
Of course, many constructors of
realistic commercial and industrial com-
pilers are doing a quite good job. They
care about correct compiling specification
and correct compiler implementation by
high level systems programs or by so-
phisticated rule sets for term or graph
rewrite systems. But there has been
bluntly no industry oriented research nor
development of techniques to implement
high level written compilers such that
their executable binary host machine ver-
sions are guaranteed to generate (at
most) correct target machine code (sec-
tion 2).
Again and again, the reason for
trouble is the use of unverified auxiliary
software like tools and in particular com-
pilers, the use of so-called software of un-
certain pedigree (SOUP, [HSE01]). There
are many examples, for instance incorrect
implementations of theorem provers or of
cryptographic protocols. Actually, even if
we (unrealistically would) assume that
compiler constructors have been verifying
their compiler programs perfectly on
source level, compiler implementations
have been and are still produced by a
now over 40 years lasting unsafe boot-
Теоретические и методологические основы программирования
24
strapping process using unverified com-
piler implementations to generate unveri-
fied compiler implementations.
In contrast to mathematicians, and
also to hardware engineers, software en-
gineers are often not so much impressed
by logical gaps, especially not by those
evoked by unverified compilers which
passed Wirth's strong compiler test.
Software constructors like to transfer
such logical gaps into Wittgenstein's do-
main of logical scepticism, arguing that
no way of reasoning will ever lead to-
wards convincing solutions (section 2).
But unverified compilers are well
outside Wittgenstein's domain and they
bear real risks (as shown by Ken Thomp-
son [Thompson84] and later by ourselves
[Goerigk99a, Goerigk99b, Goerigk00b]).
Meanwhile, since computers use to be
connected to world wide networks, we
can unfortunately not give any guarantee
for any of our programs used (section 4).
Actually, rumors say that a computer
does not survive un-hacked for more than
about eight hours continuous connection
to the internet. The risk increases, and
computer science will be accounted for
providing solutions.
The Verifix-project offers industry
oriented methods to solve the founda-
tional problem of trusted program im-
plementation, namely to produce realistic
initial compilers for diligently chosen but
nevertheless realistic programming lan-
guages, compilers that run correctly and
hence trustworthily on real host proces-
sors and generate correct and hence
trustworthy binary code for real target
processors (cf. [Goerigk/Langmaack01c]
and sections 4 to 6). Our particular tech-
nique for low level compiler implementa-
tion verification is new. It is a sophisti-
cated diagonal method of so-called syn-
tactical a posteriori-code inspection, a
variant of rigorous a-posteriori-result
checking (section 6).
Once we have got an initial cor-
rectly implemented compiler executable,
we may safely (mechanically) bootstrap
further correct compiler implementations
for instance for more comfortable lan-
guages (Bootstrapping lemma and theo-
rem, section 4). Even if the bootstrapping
compiler preserves partial correctness, it
is perfectly able to generate correct com-
piler executables which preserve total
correctness. In fact, this is a very impor-
tant point for software engineers and
process programmers interested in
trusted implementation of safety critical
embedded real-time systems.
It is by no means necessary, that
the language SL we have chosen for
trusted compiler bootstrapping is a per-
fect systems programming language.
Compilers for languages with more
elaborated data types, nested and even
higher order procedures and/or func-
tions, object-orientation and inheritance
etc. can safely be bootstrapped. SL and
its initial correct compiler implementa-
tion are chosen both to be useful tools
and to conscientiously provide a high
level proof documentation for correct low
level binary code generation. Informati-
cians can check their proof documenta-
tion rigorously even without deep
mathematical education. Moreover, if we
assume hardware to work as described in
the instruction manuals, then a lot of un-
pleasant low level checking is even re-
dundant due to our diagonal technique
(section 6).
The usual procedure, i.e. to incre-
mentally step up in a hierarchy of ab-
stractions by constructing and/or imple-
menting higher level (programming or
specification) languages safely (correctly)
on the lower level, does not work for ini-
tial correct compiler executables. The
reason is, that machines, their physics,
net lists and even their machine lan-
guages are too low level in order to ade-
quately express and to conscientiously
reason about their program behaviors
semantically. Our procedure to drive cor-
rectness down towards the real physical
machine is, and has to be, of a character-
istically different nature, namely to ex-
press and to verify realistic correct com-
pilation semantically on the upper level
first, and then to bridge the gap towards
the real machine ''in a big step''. Fortu-
nately, it turns out that our techniques
still allow to exploit the modularization in
Теоретические и методологические основы программирования
25
appropriate steps of concretization. In
fact, our intermediate languages and the
four compiler phases are carefully chosen
exactly in order to make this possible.
Theoretical basis of compiler cor-
rectness is the notion of correct relative
implementation which Verifix has devel-
oped and which is much more flexible
than classical correct implementation (cf.
[Goerigk/Langmaack01c] and section
1.1). Software engineering theory stresses
preservation of total program correctness,
but E. Börger is right in his remark (Bop-
pard, Germany, 1998): ''In the past, the
role of regular termination has been ex-
aggerated in software engineering.'' Pro-
grams need not be proved never to fail in
order to be useful. They might end in ac-
ceptable errors, and we are ''sensible
enough'' to give a guarantee that such
errors will be signaled and hence detec-
ted while programs are executed. On the
other hand, if errors cannot be detected,
for instance for undecidability reasons,
they are unacceptable and thus the user
has to avoid (circumvent) them by choos-
ing appropriate inputs. We want to admit
that this is kind of sophisticated. How-
ever, realistic software engineering requi-
rements are sophisticated trade-offs be-
tween a lot of inherently different wishes
including for instance efficiency as well.
The important point is that our results
allow, for the first time in this critical
area, to mathematically rigorously formu-
late and to formalize and prove such real-
istic requirements to be guaranteed.
It is this line of thoughts that
closes a 40 years old gap of low level
compiler implementation verification and
that makes us confident that informatics
eventually will enable to justify the con-
struction of large computer based sys-
tems. In particular, Verifix also demon-
strates techniques to incrementally trans-
fer other so far unverified software into
verified software.
Acknowledgments We would like
to thank our colleagues in the Verifix
project for many fruitful discussions, in
particular Axel Dold, Thilo Gaul, Gerhard
Goos, Andreas Heberle, Friedrich von
Henke, Ulrich Hoffmann, Vincent Via-
lard, Wolf Zimmermann. Special thanks
to Markus Müller-Olm and Andreas Wolf
for their contributions to the notion of
relative program correctness and its pre-
servation.
[Bartsch/Goerigk00d] R. Bartsch and W. Goerigk.
Mechanical a-posteriori Verification of Results:
A Case Study for a Safety Critical AI System.
In AAAI Workshop on Model Based Validation of
Intelligence MBVI'2001, Stanford, CA, U.S.A., 2001.
[Blum+89] M. Blum, M. Luby, and R. Rubinfeld.
Program result checking against adaptive pro-
grams and in cryptographic settings. In DIMACS
Workshop on Distributed Computing and Cryp-
thography, 1989.
[Cimatti+97] A. Cimatti, F. Giunchiglia, P. Pec-
chiari, B. Pietra, J. Profeta, D. Romano, and
P. Traverso. A Provably Correct Embedded Verifier
for the Certification of Safety Critical Software. In
Proceedings of CAV '97 Conference on Computer
Aided Verification, Haifa, Israel, June 1997.
[Chirica/Martin86] L. M. Chirica and D. F. Mar-
tin. Toward Compiler Implementation Correctness
Proofs. ACM Transactions on Programming Lan-
guages and Systems, 8(2):185-214, April 1986.
[Dold+02] A. Dold, W. Goerigk, F. W. von Henke,
and V. Vialard. A Mechanically Verified Compiling
Specification for a Realistic Compiler. Technical
Report UIB 2002-03, University of Ulm, 2002.
[GccBugList] Gcc Project. The Gcc Bugs Archive.
http://gcc.gnu.org/ml/gcc-bugs/.
[Goerigk96b] W. Goerigk. An Exercise in Pro-
gram Verification: The ACL2 Correctness Proof of
a Simple Theorem Prover Executable. Technical
Report Verifix/CAU/2.4, CAU Kiel, 1996.
[Goerigk97d] W. Goerigk. Towards Rigorous
Compiler Implementation Verification. In R.
Berghammer and F. Simon, editors, Proc. of the
1997 Workshop on Programming Languages and
Fundamentals of Programming, pages 118 — 126,
Avendorf, Germany, November 1997.
[Goerigk+98] W. Goerigk, Th. Gaul, and W.
Zimmermann. Correct Programs without Proof?
On Checker-Based Program Verification. In
R. Berghammer and Y. Lakhnech, editors, Tool
Support for System Specification, Development,
and Verification, Advances in Computing Science,
pages 108 — 122, Springer Verlag Wien, New
York, 1998.
[Goerigk/Hoffmann96] W. Goerigk and U. Hoff-
mann. The Compiler Implementation Language
ComLisp. Technical Report Verifix/CAU/1.7,
CAU Kiel, June 1996.
Теоретические и методологические основы программирования
26
[Goerigk/Hoffmann97] W. Goerigk and U. Hoff-
mann. The Compiling Specification from ComLisp
to Executable Machine Code. Technical Report
Nr. 9713, Institut für Informatik, CAU, Kiel, De-
cember 1998.
[Goerigk/Hoffmann98b] W. Goerigk and U. Hoff-
mann. Compiling ComLisp to Executable Ma-
chine Code: Compiler Construction. Technical
Report Nr. 9812, Institut für Informatik, CAU Kiel,
October 1998.
[Goerigk/Hoffmann98] W. Goerigk and U. Hoff-
mann. Rigorous Compiler Implementation Cor-
rectness: How to Prove the Real Thing Correct. In
D. Hutter, W. Stephan, P. Traverso, and M. Ull-
mann, editors, Applied Formal Methods - FM-
Trends 98, volume 1641 of LNCS, pages 122 —
136, Springer Verlag, 1998.
[Goerigk/Langmaack01c] W. Goerigk and
H. Langmaack. Will Informatics be able to Justify
the Construction of Large Computer Based Sys-
tems? Part I: Realistic Correct Systems Implemen-
tation. International Journal on Problems of Pro-
gramming, 2003. Forthcoming.
[Goerigk99a] W. Goerigk. On Trojan Horses in
Compiler Implementations. In F. Saglietti and
W. Goerigk, editors, Proc. des Workshops Sicher-
heit und Zuverlдssigkeit softwarebasierter Systeme,
ISTec Report ISTec-A-367, ISBN 3-00-004872-3,
Garching, August 1999.
[Goerigk99b] W. Goerigk. Compiler Verification
Revisited. In M. Kaufmann, P. Manolios, and
J S. Moore, editors, Computer Aided Reasoning:
ACL2 Case Studies. Kluwer Academic Publishers,
2000.
[Goerigk00a] W. Goerigk. Trusted Program Exe-
cution. Habilitation thesis. Techn. Faculty, Chris-
tian-Albrechts-Universität zu Kiel, May 2000.
To be published.
[Goerigk00b] W. Goerigk. Proving Preservation of
Partial Correctness with ACL2: A Mechanical
Compiler Source Level Correctness Proof. In M.
Kaufmann and J S. Moore, editors, Proceeding of
the ACL2'2000 Workshop, University of Texas,
Austin, Texas, U.S.A., October 2000.
[Goos/Zimmermann99] G. Goos and W. Zimmer-
mann. Verification of Compilers. In E.-R. Olderog
and B. Steffen, editors, Correct System Design,
volume 1710 of LNCS, pages 201 — 230. Springer
Verlag, 1999.
[Gaul+99] Th. Gaul, W. Zimmermann, and W. Go-
erigk. Construction of Verified Software Systems
with Program-Checking: An Application To Com-
piler Back-Ends. In A. Pnueli and P. Traverso, edi-
tors, Proc. FLoC'99 International Workshop on Run-
time Result Verification, Trento, Italy, 1999.
[Heberle+98]A. Heberle, Th. Gaul, W. Goerigk,
G. Goos, and W. Zimmermann. Construction of
Verified Compiler Front-Ends with Program-
Checking. In Proceedings of PSI '99: Andrei Er-
shov Third International Conference on Perspec-
tives Of System Informatics, volume 1755 of Lec-
ture Notes in Computer Science, Novosibirsk, Rus-
sia, 1999. Springer Verlag.
[Hoffmann98b] U. Hoffmann. Compiler Implemen-
tation Verification through Rigorous Syntactical
Code Inspection. PhD thesis, Technische Fakultät
der Christian-Albrechts-Universität zu Kiel, Tech-
nical Report 9814, 1998.
[HSE01] C. Jones, R.E. Bloomfield, P.K.D. Froo-
me, and P.G. Bishop. Methods for assessing the
safety integrity of safety-related software of un-
certain pedigree (SOUP). Contract Research Re-
port 337/2001, Health and Safety Executive, Ade-
lard, London, UK, 2001.
[Kaufmann/Moore94] M. Kaufmann and
J S. Moore. Design Goals of ACL2. Technical Re-
port 101, Computational Logic, Inc., August 1994.
[Langmaack97a] H. Langmaack. Softwareengi-
neering zur Zertifizierung von Systemen: Spezifi-
kations-, Implementierungs-, Übersetzerkorrek-
theit. Informationstechnik und Technische Infor-
matik it+ti, 39(3):41—47, 1997.
[Langmaack97b] H. Langmaack. The ProCoS Ap-
proach to Correct Systems. Real Time Systems,
13:251—273, Kluwer Academic Publishers, 1997.
[Langmaack97c] H. Langmaack. Contribution to
Goodenough's and Gerhart's Theory of Software
Testing and Verification: Relation between Strong
Compiler Test and Compiler Implementation
Verification. Foundations of Computer Science:
Potential-Theory-Cognition. LNCS 1337, pages
321—335, Springer Verlag, 1997.
[Loeckx/Sieber87] Jacques Loeckx and Kurt
Sieber. The Foundations of Program Verification
(Second edition). John Wiley and Sons, New
York, N.Y., 1987.
[Moore88] J S. Moore. Piton: A verified assembly
level language. Techn. Report 22, Comp. Logic
Inc, Austin, Texas, 1988.
[Moore96] J S. Moore. Piton: A Mechanically
Verified Assembly-Level Language. Kluwer Aca-
demic Press, Dordrecht, The Netherlands, 1996.
[Mueller-Olm/Wolf99] M. Müller-Olm and
A. Wolf. On Excusable and Inexcusable Failures:
Towards an Adequate Notion of Translation Cor-
rectness. In J. M. Wing, J. Woodcock, and
J.Davies, editors, Proceedings of Formal Methods
FM'99, volume 1709 of LNCS, pages 1107—1127,
Toulouse, France, 1999. Springer Verlag.
Теоретические и методологические основы программирования
27
[Nielson/Nielson92] H. R. Nielson and F. Nielson.
Semantics with Applications: A Formal Introduc-
tion. John Wiley & Sons, Chichester, 1992.
[Pnueli+98] A. Pnueli, M. Siegel, and E. Singer-
man. Translation Validation. In Proc. 4th Interna-
tional Conference on Tools and Algorithms for the
Construction and Analysis of Systems, Lisbon, Por-
tugal, March 1998.
[Thompson84] K. Thompson. Reflections on
Trusting Trust. Communications of the ACM,
27(8):761—763, 1984. Also in ACM Turing Award
Lectures: The First Twenty Years 1965-1985, ACM
Press, 1987, and in Computers Under Attack: In-
truders, Worms, and Viruses, ACM Press, 1990.
[Wirth77] N. Wirth. Compilerbau, eine Ein-
führung. B.G. Teubner, Stuttgart, 1977.
[Wolf00] A. Wolf. Weakest Relative Precondition
Semantics - Balancing Approved Theory and Real-
istic Translation Verification. PhD thesis, Tech-
nische Fakultät der Christian-Albrechts-
Universität, Report No. 2013, Kiel, February 2001.
Date received 20.03.03
About authors
Prof. Dr. Wolfgang Goerigk
Professor of Institute of Informatics and
Applied Mathematics
Prof. Dr. Hans Langmaack
Professor of Institute of Informatics and
Applied Mathematics
Institut für Informatik und Praktische Mathematik
Christian-Albrechts-Universität zu Kiel, Kiel,
Germany
Email: wg@informatik.uni-kiel.de,
hl@informatik.uni-kiel.de
|