1
OpenTC Newsletter
January 2008
From the Open Trusted Computing (OpenTC) research project, sponsored by the
European Union.
In this issue:
- Editorial: Verified compartments to protect users against malware
- Private Electronic Transactions - The OpenTC proof-of-concept prototype
- Static analysis using Abstract Interpretation (part 2)
- Recent OpenTC publications
Editorial: Verified compartments to protect users against malware
By: Arnd Weber, ITAS, Forschungszentrum Karlsruhe, Germany
Dear reader,
At the beginning of the OpenTC project, many opinions on Trusted Computing (TC) gathered
on the Internet in discussion fora and articles were critical of the technology. Some people
believed that TC would be used for tracking citizens’ activities, locking computers into
proprietary configurations, enforcing unfair business models for content or software
provision, and even automatically deleting emails and documents without the user’s approval.
In this context, the project’s work package on requirement analysis (WP02) found that a
prototype showing TC's potential to protect users could be used to make TC more attractive,
as opposed to an application protecting "only" organisations like employers or content
providers. Such a prototype would make it possible to demonstrate to the public the broad
range of purposes for which TC can be used. A particularly suitable use-case in our opinion is
one that demonstrates how TC can be used to protect individuals against financial risks, e.g.,
security threats in homebanking or online auctions. Given that computer criminals frequently
produce malware software to fool users into giving them their security credentials, so-called
phishing, strong protection against such attacks would be the objective of a suitable use-case
implementation. On the basis of the OpenTC architecture, the design of the prototype would
comprise a TC-secured hypervisor with a verified compartment running an isolated browser,
to be used for the risky transactions underlined in the scenario (i.e., not for general web
surfing) in order to keep it secure. This compartment would run next to a compartment with a
legacy operating system and untrusted applications used for casual tasks. We nicknamed this
prototype the "PET", an abbreviation of "Private Electronic Transactions", and the consortium
implemented a proof-of-concept prototype based on this scenario.
The PET prototype is described in the first article by Stephane Lo Presti (Royal Holloway,
University of London), Gianluca Ramunno (Politecnico di Torino), and Dirk Kuhlmann
(Hewlett Packard Laboratories, Bristol). The design and decision process which led to
creating the PET is described in more detail in Kuhlmann/Weber [1], where the reader can
find a review of the various arguments found in the media, a description of the consortium’s
internal decision process, and the conclusions drawn from this process, as well as information
on the OpenTC architecture and PET design. The source code has been made publicly
2
available [2] in order to enable developers, in particular FOSS (Free and Open Source
Software) developers, to use it.
In future real-world systems that use the code produced by the OpenTC project, the various
mechanisms from the OpenTC architecture should be implemented at a very high level of
quality. In the second article in this OpenTC newsletter, we continue our description of the
consortium’s approach to improving the source code of the project. In the last issue, Pascal
Cuoq from CEA-LIST, Paris, provided an introduction to "Static analysis using Abstract
Interpretation", while in this second part of his article he goes on explaining precisely how
static analysis works. The consortium’s approach to the trustworthiness of code will continue
to be explored in upcoming articles in the next issues of the OpenTC newsletter.
We conclude this newsletter with an announcement of a new research paper published by
members of the OpenTC consortium.
References:
- [1] Kuhlmann, Dirk; Weber, Arnd (eds.): Requirements Definition and Specification.
OpenTC Project Deliverable D02.2.
http://www.opentc.net/deliverables2006/OTC_D02.2_Requirements_Definition_and_Specific
ation_update.pdf
- [2] Free and Open-Source Software (FOSS) components of the Open Trusted Computing
architecture:
http://www.opentc.net/index.php?option=com_content&task=view&id=47&Itemid=65
Contact: arnd.weber at itas.fzk.de
Our thanks go to Richard Brown, Alison Hepper, Dirk Kuhlmann, Stephane Lo Presti and
Dirk Weber for their help in preparing this issue.
Private Electronic Transactions - The OpenTC proof-of-concept prototype
By: Stephane Lo Presti, Royal Holloway, University of London, UK; Gianluca Ramunno,
Politecnico di Torino, Italy; and Dirk Kuhlmann, Hewlett Packard Laboratories, Bristol, UK
Introduction
---------------
The OpenTC project recently published the first proof-of-concept prototype of its Open
Trusted Computing architecture. This work involved several developers from HP (United
Kingdom), IBM (Switzerland), Politecnico di Torino (Italy), Ruhr-Universitaet Bochum
(Germany), Technische Universitaet Dresden (Germany), IAIK Graz University of
Technology (Austria) and SuSE (Germany). The prototype aims to demonstrate some core
ideas of the OpenTC approach, combining Trusted Computing (TC) and virtualisation
technologies with Free and Open Source Software (FOSS) development. The release
implements a concrete application of TC, is available to the general public, and could serve as
a working basis for interested developers.
As a proof-of-concept prototype, the implementation is far from comprehensive, and has not
been thoroughly tested. It does not include all the necessary components for the OpenTC
architecture, nor are the existing ones in any finalised form. Nevertheless, we hope that the
proof-of-concept work will give some impression of how TC could be applied in practice,
3
foster discussions about the use of TC and the OpenTC architecture, and encourage
contributions from the FOSS communities. With some minor exceptions, all source code is
released under the GPLv2 license. It is provided as both a Live CD image (binaries) and as
source code (see link at the end of the article). The prototype was developed and tested on HP
nx6325 and IBM T60 laptops equipped with Trusted Platform Modules (TPMs) v1.2 and 1
GB RAM.
OpenTC makes use of virtualisation layers - also called Virtual Machine Monitors (VMMs)
or hypervisors - and supports two different implementations (i.e., Xen and L4/Fiasco). This
layer hosts compartments, also called virtual machines (VMs), domains or tasks, depending
on the VMM being used. Some domains host trust services that are available to authorised
user compartments. Various system components make use of TPM capabilities, e.g., in order
to measure other components they depend on or to prove the system integrity to remote
challengers.
The current prototype implements a scenario called Private Electronic Transactions (PET),
which aims to improve the trustworthiness of interactions with remote servers. Transactions
are simply performed by accessing a web server through a standard web browser running in a
dedicated trusted compartment named "domT". In the PET scenario, the server is assumed to
host web pages belonging to a bank; however, the setup also applies to other e-commerce
services.
The communication setup between browser compartment and server was extended by a
protocol for mutual remote attestation tunnelled through an SSL/TLS channel. During the
attestation phase, each side assesses the trustworthiness of the other. If this assessment is
negative on either side, the SSL/TLS tunnel is closed, preventing further end-to-end
communication. If the assessment is positive, end-to-end communication between browser
and server is enabled via standard HTTPS tunnelled over SSL/TLS.
General approach
---------------------
The approach of this scenario relies on four elements:
1) Trusted platform setup
2) Authenticated boot process
3) Registration of the known-good measurement values
4) Trusted communication setup
The following sections give a cursory overview of these steps.
1. Trusted Platform Setup
As a first step, the user has to initialise the client platform and to prepare it for subsequent
operations.
The setup procedure is performed as soon as the OpenTC system has started up for the first
time. First, the user, acting as the platform owner, must "take ownership" of the TPM. This
assumes that the TPM is enabled in the BIOS and, if it was already used before, is cleared and
re-enabled. More information about this feature of TC can be found at [1].
Next, an Attestation Identity Key (AIK) must be created and certified, and the corresponding
4
identity activated. In a real-world situation, Privacy Certification Authorities (PCAs) that
operate a valid TC-enabled Public Key Infrastructure (PKI) would be used during this
process. However, for the sake of simplicity, both the requests for and the release of the AIK
certificate operations are currently handled locally on the client, using hard-coded passwords.
This is done by a software library that comes with hard-wired mock certificates for the
authorities involved (e.g., PCA).
2. Authenticated boot process
From the initial bootup process up to the start of trusted components, a chain of trust is
generated: each component of the chain is measured prior to passing control to it. The
component measurements, i.e. their fingerprints through cryptographic hashes of relevant
binary and configuration data, are accumulated in Platform Configuration Registers (PCRs) of
the TPM.
In order to generate the chain of trust, all components in this chain must be instrumented to
perform integrity measurements of their successors in execution. For instance, the BIOS must
include a Core Root of Trust for Measurement (CRTM), as defined by the Trusted Computing
Group. Further modifications concern the Master Boot Record (MBR) and the boot loader.
The latter has to measure the hypervisor, the kernel and initial ram disk images of privileged
domains, or files or disk images of trusted compartments. For this purpose, the OpenTC
prototype includes "tGRUB", an extended version of the familiar GRand Unified Bootloader
(GRUB). The tGRUB boot menu offers a choice between the two different virtualisation
layers, XEN and L4/Fiasco.
A second boot menu option concerns the execution mode. It offers a "normal user" mode that
comes with a simplified interface and restricts access to management functions, geared
towards showing how the user can perform a transaction in a real-life scenario. The "expert
user" mode, on the other hand, enables full access to management features, permitting a peek
“under the hood”. It allows interactive access and comes with a more complex interface. As a
demonstration of the differences between successful and failing verification of integrity
measurements, the boot menu also provides a "good domT" and a "rogue domT" option. In
the "good" mode, all measurements match their expected values. On the other hand, the
"rogue" mode simulates a modified compartment that could have been tampered with by an
attack from a malicious program. In this case, at least one PCR contains an unexpected
measurement value.
OpenTC’s tGRUB loader is constrained to supporting the so-called Static Core Root of Trust
for Measurement (S-CRTM) model. In this case, all security and trust-relevant components
must be measured, starting with the BIOS. To demonstrate the new Dynamic Core Root of
Trust for Measurement (D-CRTM) approach introduced with TPM v1.2, OpenTC provides
the Open Secure LOader (OSLO) boot loader implemented as a standard module for
GRUB/tGRUB. OSLO implements the D-CRTM for AMD's CPUs, invoking the SKINIT
instruction for re-initialising the platform in a trustworthy manner late at runtime.
3. Registration of the Known-Good Measurement Values
The client can now register with a server by uploading the measurements that represent its
platform state (that is assumed to be trusted). During this procedure, the user (acting as a bank
operator) registers his platform with a bank server. To this end, he uploads the integrity
measurements of his platform (i.e., the expected value for the domT compartment), thus
5
authorising the trusted compartment to connect to the bank server. In a realistic scenario, this
process would be automated using secure communications and a dedicated registration
protocol. Since the prototype does not yet implement this feature, the user instead launches a
script (in "normal user" mode) or uses a browser (in the "expert user" mode) to upload a file
containing a measurement digest to the front-end proxy running on the bank server. This
digest corresponds to the current state of the client platform, i.e., its trusted virtualisation layer
and the trusted domain domT. For simplification, the bank server (named "domS")
measurements are already present on the client side (in a privileged compartment of the
virtualisation layer named Domain-0 or dom0) of the OpenTC system: the PCR metrics
defined to correspond to a "trusted" server state are currently hard-wired into the system.
4. Trusted communication setup
Trust status information is exchanged between the client and the server through a pair of
proxy services running in a privileged compartment (dom0) on the client and as a front-end in
the server compartment (domS). The proxies communicate through an SSL/TLS tunnel that
can encapsulate any TCP-based protocol. For the PET scenario, HTTPS is used.
The communication setup is initiated when the browser is started in the trusted compartment
(domT) and the link provided in its toolbar clicked on. The connection request is passed to the
client proxy that runs in the privileged compartment (dom0). A dedicated component running
in this compartment opens an SSL/TLS tunnel to connect to the server-side proxy running in
the bank server compartment (domS). The permissibility of this connection must be stated in
the policy of the virtualisation layer. Measurements of software components on both sides
(client and server, see above) are represented by PCR values of the hardware and software
TPM. These values are signed with the AIK acquired in step 3, and communicated to the
respective peer system.
Communication between the client and the server will only be enabled if both the client and
the server metrics suggest that they booted into (and still run) the expected configuration. This
could prove a countermeasure to phishing attacks, preventing the user from following a false-
lead URL to connect to a fake bank server. The mechanism might also improve the protection
of the bank server against unauthorised connections.
Platform components and behaviour
-------------------------------------------
The authenticated boot process launches the selected virtualisation layer, which is responsible
for controlling four dedicated compartments, namely:
- A privileged compartment (called "dom0") that directly accesses the physical platform and
includes the drivers for hardware devices. This compartment is also used to perform
management operations at the virtualisation layer. In "normal user" mode, this compartment is
not visible, whereas the "expert user" mode allows client compartments (see below) to be
started manually via scripts. Dom0 is part of the Trusted Computing Base (TCB).
- A compartment for the server side of the demonstrator (called "domS") which executes the
banking application and its front-end. It locally simulates a remote server (web server and
proxy). For the prototype, this removes the dependency on external communication which
would require an additional, separate banking computer. The domain is accessed via the
network name "domSbox", and a software TPM emulator is used to perform the integrity-
related operations for this domain. The compartment is not visible to the user. It goes without
6
saying that this domain could equally be executed on a remote physical machine, and future
versions of the OpenTC prototype will support this.
- Two compartments for the client side of the system. The first compartment (called "domT")
solely provides web browsing as its single functionality. It is considered trusted in that its
integrity has been measured and the values correspond to a well-known configuration.
Measurements, which include the configuration file, the kernel and the virtual disk image with
the root file system, are accumulated within PCR[11] in the TPM through the “PCR extend”
operation. The second compartment is an untrusted one (called "domU"). It is not measured
and is intended for daily use, but specifically not for the PET transaction.
The platform policy ensures that only the trusted compartment (domT) is authorised to use the
client proxy (executing in the privileged compartment dom0) for connecting to the bank
server (executing in domS). By contrast, the untrusted compartment (domU) cannot connect
to the bank server, since no measurements exist that can be used to attest to its trusted state.
Client compartments run a stripped-down Linux system (a Debian-based Damn Small
Linux/DSL distribution), while the privileged compartment dom0 runs either a SuSE or a
DSL distribution, depending on which version of prototype is used. The server compartment
(domS) runs a standard Debian distribution.
The L4-based OpenTC implementation provides a secure GUI service for managing input and
output. This GUI is provided as a trusted service started by tGRUB at boot time and running
in a dedicated compartment. The top part of the display is reserved to indicate the number of
active compartments and the name of the one currently hooked to the display. This section of
the screen is considered trusted because it is under the exclusive control of the secure GUI.
With the L4 virtualisation layer, a pair of hotkeys are used to switch between compartments.
For the Xen-based OpenTC implementation, the whole screen is under the control of a
selected compartment. Each compartment is assigned a fixed hotkey. When a specific hot key
associated to a compartment is pressed, the user can be sure that the desired compartment will
actually be displayed since the key is under the exclusive control of the privileged
compartment dom0.
Shortcuts, simplifications, and limitations
--------------------------------------------------
Trusted Computing is an emerging technology, and infrastructure support, e.g., for issuing
certificates, does not yet exist. The technology is also fairly complex. For example, first-time
users are easily confused by the multiplicity of authorisation secrets. For the sake of
simplicity, the OpenTC prototype, therefore, uses fixed passwords as authorisation secrets for
the TPM and AIK keys (which can, of course, be changed for all operations by editing the
configuration scripts in the "expert user" mode).
The prototype attempts to strike a balance here in providing all necessary components
(including PKI mechanisms) as part of the distribution. In particular, the server-side
mechanisms reside in a dedicated compartment on the same physical hardware that runs the
client.
The PCR metrics corresponding to a trusted PKI server state are currently hard-wired into the
PKI component running on the client system. The banking compartment domS is not actually
measured since it employs a TPM emulator instead of a hardware TPM. Instead, we just
7
communicate the initial PCR values of the software TPM. In a future release of the OpenTC
prototype, the server side will run on a different physical platform, and integrity
measurements of the server domain will be duly recorded.
In the "rogue domT" scenario, the measurement of the client banking compartment (domT)
does not correspond to the one uploaded earlier to the bank server. Consequently, the
attestation will fail, and communication with the bank server will be disallowed. Due to
implementation specifics, the PCRs mismatch currently has to be simulated in that the values
are not generated from actual measurements of the persistent compartment image but only
from a different configuration file for domT. A future release will fix this issue.
Furthermore, the current prototype is also limited in that man-in-the-middle or "relay of
attestation challenge" attacks have not yet been considered. For more information, please see
[2].
Outlook
---------
Although the current implementation of the PET scenario is relatively straightforward and
cuts quite a number of corners, it is a concrete example of the possibilities of coupling TC
with virtualisation technology. As the source code of the prototype is publicly available, the
OpenTC prototype provides a working basis for any developer interested in implementing TC
applications.
About the authors: Stephane Lo Presti is a research assistant working at Royal Holloway,
University of London (UK), on mobile trusted computing and dissemination activities of the
OpenTC project. Gianluca Ramunno is a research assistant working at the technical university
Politecnico di Torino (IT) on security applications and PKI for trusted computing. In the
OpenTC project, he coordinated the development of the proof-of-concept prototype related to
the PET scenario. Dirk Kuhlmann is a senior research engineer for Hewlett Packard
Laboratories in Bristol, UK, where he works as a member of the Trusted Systems Laboratory.
He acts as the overall technical leader for the OpenTC project.
Download:
The prototype can be downloaded from the OpenTC website, URL:
http://www.opentc.net/index.php?option=com_content&task=view&id=45&Itemid=63
The source code for the components of the OpenTC system is referenced in the following
webpage:
http://www.opentc.net/index.php?option=com_content&task=view&id=47&Itemid=65
References:
- [1] "The Roots of Trust - The RTM and the TPM ", Eimear Gallery. Second Lecture of the
Trusted Computing course, MSc of Information Security, Royal Holloway, University of
London, 2007.
- [2] Kenneth Goldman, Ronald Perez and Reiner Sailer: Linking remote attestation to secure
tunnel endpoints. In: Proceedings of the first ACM workshop on Scalable Trusted Computing
(STC '06), pp. 21-24. Alexandria, Virginia, USA, 2006. ACM Press, ISBN: 1-59593-548-7,
http://doi.acm.org/10.1145/1179474.1179481
.
Contacts: Stephane.Lo-Presti at rhul.ac.uk; Ramunno at polito.it
8
Static analysis using Abstract Interpretation (part 2)
By: Pascal Cuoq, Commissariat à l'Energie Atomique (CEA-LIST), Paris, France
This is the second part of the article, the first part of which was published in the September
2007 issue of the OpenTC newsletter, see [1].
The sample program analysis used in the first part of the article showed how static analysis
can work at first sight. This second and final part of the article aims to show that it is not
always as easy as it seems, using various program examples.
The property of termination of a program
The programming example used in the first part of the article was simple, but not simplistic,
because it contained a loop statement. Many research developments in theoretical computer
science either have to do with the fact that loop statements are necessary for programming, or
try to deal with the difficult questions they automatically raise. One such question is whether
a given program is always guaranteed to end and return a result. This property is considered
particularly interesting and is called "termination" of the program. However, it was not
difficult to check the properties of the loop statement (a 'while' statement) used in the previous
programming example. It is easy to see that the condition in the 'while' construct (x >= 2)
would eventually become false and cause the loop to stop, meaning that the program would
not run forever. Let us now consider the following C example instead:
1 for (n = 4 ; ; n += 2)
2 {
3 for (p1 = 2 ; p1 < n ; p1 ++)
4 {
5 p2 = n - p1;
6 if (is_prime(p1) && is_prime(p2))
7 break;
8 }
9 if (p1 == n)
10 break; // sum of two primes not found for n.
11 }
The function "is_prime" always terminates and returns "true" when its argument is a prime
number. The implementation of this function requires some ingenuity in order to make it
efficient for big numbers, but a simple implementation that repeatedly divides its argument
"m" by every number smaller than m and returns "true" only if none was a divisor, would be
enough for our purposes. Programming this function in C is left as an exercise to the reader.
The above program enumerates for each value of the variable "n" the even integers greater
than 2 (4, 6, 8, 10, etc.). For each of these successive values of n, the program first (lines 3 to
8) enumerates the various ways of splitting n into the sum of two integers p1 and p2. If this
split is such that both p1 and p2 are prime numbers, the program jumps to the next even value
for n (line 7). If no pair of numbers p1 and p2 satisfying this property, i.e., n == p1 + p2 and
p1 and p2 both prime, is found, the program stops (line 10).
9
This program is very simple, but in fact conceals a very difficult theoretical problem: deciding
whether the program terminates or not is equivalent to proving or disproving the mathematical
"Goldbach's conjecture", which at the time of this writing remains an open problem in number
theory and has been so for more than 250 years. In practice, this means that it is in the worst
case impossible to know whether a program will stop under any circumstances. Although the
previous program does not use any complicated programming features, the question of
whether it terminates or not is theoretically even harder to solve than Fermat's last theorem.
Loop invariants
Even when the termination of a loop statement is easier to establish than in the previous
example, the correct behaviour of the loop may rely on complicated hidden invariants. "Loop
invariant" is the name given to a property that holds throughout the execution of a loop. This
situation should be familiar to any developer who has ever had to modify code that he did not
write himself: the program works for reasons that are not obvious in the code, for example
because the value of a certain variable "p" can never be negative. The invariants are not
always explicitly written in the program (experienced developers write them in comments or
in assertions, but even with experience, it is not easy to think of all the invariants that should
be written down). Taking the example of the variable p that is always positive, the invariant
holds because one can check on each program statement that a negative value is never
assigned to p. The difficulty lies in the fact that it is not easy to reconstruct the invariant by
simply looking at the source code. Similarly to the situation of the termination of loop
statements, it can in fact be arbitrarily difficult.
Analysis of actual source code does not always require proving or disproving Goldbach's
conjecture, however. The above example is only intended to show the kind of difficulties that
make the problem impossible to solve in all generality. In real life and for ordinary programs,
invariants are often simple enough to be discovered automatically.
Example of a program that is difficult to analyse
Besides loop statements, real programs also contain many statements that are difficult to
handle because they do not fit well into the theoretical frameworks used for program analysis.
The particular set of statements that causes problems depends on the analysis framework, but
it typically contains some or all of the following: casts, union types, architecture-dependent
statements, pointers and aliasing, integer overflows, floating-point arithmetic. The following
example illustrates several of the above issues:
1 void shift_string (char *s, unsigned int src_offs, unsigned int size)
2 {
3 unsigned int dst_offs = src_offs - 4;
4 while (size > 0)
5 {
6 * (int *) (s + dst_offs) = * (int *) (s + src_offs);
7 size -= 4;
8 dst_offs += 4;
9 src_offs += 4;
10 }
11 }
10
This function makes particular assumptions about the computing architecture and the
compilation model in order to shift a specified part of a string "s" (starting at "src_offs") by
four characters. The function also assumes that the variable "size" is a multiple of 4, and that
the parameters passed to it do not make it access memory out of bounds or in a misaligned
way. For the purpose of the program analysis, we assume that these assumptions are well
understood by the developer, and that the bug we are looking for (if any) does not lie in these
assumptions. Proving that the above function satisfies its informal specification (shifting part
of the string "s" by four characters) is difficult. Besides all the low-level statements that the
analyser needs to understand (e.g., the conversion from "char*" to "int*"), there are several
hidden invariants that ensure that the function works as intended.
To perform the analysis of this program, let us focus first on one of these invariants: at the
beginning of the body of the loop (line 6), the current value of variable "dst_offs" is always
equal to "src_offs-4".
It is necessary to establish this invariant in order to prove that the function "shift_string"
operates as it is supposed to. For a 32-bit architecture, the property implies, in particular, that
there is no overlap between the four bytes read at the address "s+src_offs" and the four bytes
written at "s+dst_offs" (line 6).
The equality "dst_offs = src_offs - 4" can be automatically discovered by relational abstract
interpretation. The idea behind relational abstract interpretation is to compute information
about the relationships that are guaranteed to hold between the values of several variables, in
addition to sets of possible values for individual variables. Sets of possible variable values are
propagated from instruction to instruction in the same fashion that intervals were propagated
in the first part of the article. But "values" here means possible values for the tuple of
variables (size, dst_offs, src_offs). In the first part of the article, we restricted the "sets" of
values to intervals. Here, we also need to make a choice regarding the representation of these
sets of possible tuples, so that they can be computed in a reasonable amount of time and
memory. There is a wide selection of options when choosing a representation for sets of
tuples, but we are only going to consider linear relations between two variables (e.g.,
y=a*x+b), because this representation is space-efficient and simplifies the computations.
Without precise knowledge of the values of the arguments "src_offs" and "size", we know
that values that do not satisfy the above equality are impossible for the pair (src_offs,
dst_offs) after executing line 3. In fact, the values that are possible for the pair can be
represented as a linear relation between these two variables: src_offs = dst_offs + 4.
Given these values for the pair (src_offs, dst_offs), the condition of the 'while' -loop can both
be true or false, so we have to assume that this state may propagate to both the inside of the
loop at line 6 and the exit of the loop (line 11), which is also the exit of the function.
We will assume that the instruction on line 6 does not affect the values of variables src_offs
and dst_offs (this would theoretically require proof that the memory access "*(int *)(s +
dst_offs)" is not out-of-bounds). Line 7 does not change the relation between src_offs and
dst_offs either.
The instruction on line 8 has an effect on the value of dst_offs and, therefore, on the relation
between src_offs and dst_offs. Fortunately, the effect of this instruction on the relation
between src_offs and dst_offs can be computed. Better yet, the resulting state can be
represented as another linear relation, "src_offs = dst_offs".
11
The instruction on line 9 has an effect on the relation between src_offs and dst_offs, too.
Since this assignment increments the value of src_offs by 4, its effect on a state where
"src_offs = dst_offs" is to produce a state where "src_offs = dst_offs + 4" (since the new
src_offs is the same as the old src_offs plus 4).
The state of the variables at the end of line 9 cannot be used to decide whether the condition
of the 'while' loop (size > 0) is true, so this state must be propagated again to both the exit of
the function and the beginning of the body of the loop. This state, which is identical to the
state that occurred after executing line 3, has in fact already been propagated to the exit of the
function and the beginning of the body of the loop. This means that this state is a fixpoint of
the program (i.e., a state that leads to itself when the body of the loop is applied to it), and that
the program analysis is finished. The analysis has determined that the property held, because
the fixpoint found represents the invariant we wanted to prove.
The choice of the kind of sets that are used determines the types of programs that can be
analysed accurately. In the above example, linear relations are a good choice because:
1. Some variables in the program are in a linear relation to each other, and
2. The instructions executed by the program (particularly, at lines 8 and 9) transform a linear
relation into another linear relation, which can also be represented.
What else is necessary to analyse this program?
The other important requirement in order to be able to analyse this program is a memory
model. Actually running the program would have allocated the string "s" to somewhere in the
memory, and it would be possible to analyse the function "shift_string" with respect to this
particular memory allocation (in this case, a particular choice of address where "s" is stored).
But this is not satisfactory because the goal of static analysis is to check that there are no
errors for all possible executions, which means not only for all inputs, but also for all
addresses at which the system decides to allocate string "s". If two strings are allocated in the
program, one goal of the verification process would be to check that one string is not modified
via an out-of-bounds access to the other. This error may manifest itself for some allocations
while it may not be visible for others, making it hard to find or debug solely by testing the
program.
For this reason, the static analysis of a program proceeds with respect to an abstract memory
model. An abstract memory model allows manipulation of a synthetic representation of all
possible choices for the layout of a program's data in memory. As with the choices that must
be made with respect to the representation of relationships between variables, there are
compromises in the design of an abstract memory model. It goes beyond the scope of this
article to delve into all the various possibilities. The purpose of an abstract memory model, on
the other hand, is simple: the abstract memory model should make it possible to analyse a
program without having to choose a particular memory allocation. Instead, when the memory
model is appropriately devised, a program property proved in the abstract memory model
holds for all the possible allocations that can occur at run-time. The adjective "correct", which
was applied to analyses in the first part of the article, is applied to abstract memory models
which have this property. Of course, one needs a correct memory model in order to build a
correct analyser.
In the previous example, it is the task of the memory model to ensure that the instruction on
line 6 does not have any effect on the relation between src_offs and dst_offs. Because the C
12
programming language is a low-level language, an out-of-bounds access does not necessarily
translate into a run-time error. Depending how the program's data is laid out in memory, the
memory access could also silently change the value of another arbitrary variable. A
reasonable memory model should exclude this possibility, and instead emit a warning
concerning the out-of-bounds access, if one might exist.
To analyse this example precisely, the memory model also needs to describe the fact that an
"int" variable takes up the same space as four "char" variables (on most current computers,
integers are stored on 32 bits while characters require 8 bits), and what exactly happens when
a "pointer to char" is cast into a "pointer to int", and subsequently accessed.
The Frama-C toolbox
The Laboratory for Software Safety at CEA LIST (Paris, France) is developing Frama-C, a
toolbox for the static analysis of C programs. This toolbox is designed to enable different
analysis techniques and features to be plugged in, and used with each other. One of the
distinguishing features of the Frama-C toolbox is the specification of the memory model,
which is especially adapted to the analysis of embedded (low-level) C code. Frama-C has
been used to analyse parts of the Xen hypervisor in the context of the OpenTC project.
Editor's note: An article about the analysis of the XEN hypervisor will be published in a
future issue of the OpenTC newsletter.
About the author: Pascal Cuoq has been playing with computers since he was 6. He is
currently doing so at CEA-LIST, within the Software Safety Laboratory, where he is one of
the architects of Frama-C, an assistance tool to improve confidence in critical C code.
Contact: pascal.cuoq at cea.fr
Reference:
[1] Static analysis using Abstract Interpretation. In: OpenTC newsletter of September 2007:
http://www.opentc.net/publications/OpenTC_Newsletter_02.html#link3
Recent OpenTC publications
Since the publication of the last newsletter, the OpenTC project partners have produced one
scientific publication:
- Murray, D.; Milos, G.; Hand, S.: Improving Xen security through disaggregation. In
Proceedings of the 4th international conference on Virtual Execution Environments (VEE
2008), March 2008 (to appear).
Edited by the Institute for Technology Assessment and Systems Analysis,
Forschungszentrum Karlsruhe, Germany, on behalf of the OpenTC research project
consortium, in co-operation with all partners.
Editor: Arnd Weber, Forschungszentrum Karlsruhe GmbH, ITAS, Hermann-von-Helmholtz-
Platz 1, D-76344 Eggenstein-Leopoldshafen, Telephone: + 49 7247 82 3737.
Contact: editor at opentc.net
13
Disclaimer: The views and opinions expressed in the articles do not necessarily reflect those
of the European Commission and the consortium or partners thereof. All articles are regarded
as personal statements of the authors and do not necessarily reflect those of the organisation
they work for.
The OpenTC-project is a research project supported by the European Commission, project
IST-027635. Its 23 partners are: Technikon Forschungs- und Planungsgesellschaft mbH
(project coordination, AT); Hewlett-Packard Ltd (technical leader, UK); AMD Saxony LLC
& Co. KG (DE); Budapest University of Technology and Economics (HU); Commissariat à
l’Energie Atomique – LIST (FR); COMNEON GmbH (DE); Forschungszentrum Karlsruhe
GmbH – ITAS (DE); Horst Goertz Institute for IT Security, Ruhr-Universitaet Bochum (DE);
IBM Research GmbH (CH); Infineon Technologies AG (DE); INTEK Closed Joint Stock
Company (RU); ISECOM (ES); Katholieke Universiteit Leuven (BE); Politecnico di Torino
(IT); Portakal Teknoloji (TR); Royal Holloway, University of London (UK); SUSE Linux
Products GmbH (DE); Technische Universitaet Dresden (DE); Technische Universitaet Graz
(AT); Technische Universitaet Muenchen (DE); Technical University of Sofia (BR);
TUBITAK – UEKAE (TR); and University of Cambridge (UK).
For more information about the project, see:
http://www.opentc.net
Feedback to the consortium:
http://www.opentc.net/feedback
Archive of newsletters:
http://www.opentc.net/newsletter
Subscription: To subscribe or unsubscribe to the newsletter, write an email to <subscribe at
opentc.net> or <unsubscribe at opentc.net>.