Framework for Design Validation of Security Architectures Page: 11
The following text was automatically extracted from the image on this page using optical character recognition software:
when an adversary has physical possession of the SP
device. Therefore, for step 1, we attempt to replace
the TSM by installing a new DRK which signs different
TSM code, however it then cannot access the author-
ity's data which was protected by the original DRK.
Since the DRK never leaves the processor chip and can-
not be extracted, there is no other way to get access to
the original DRK.
In step 2, the integrity of a TSM must be protected both
before and during execution. This involves testing SP's
hardware protection of the confidentiality and integrity
of all intermediate data that it generates. This inter-
mediate data can be attacked while in general registers
during a processor interrupt or in secure memory at any
time while the TSM is not running. Additionally, the
SP master secrets themselves must only be used by the
TSM itself and not other software. The code integrity
of the TSM must be protected both on disk and during
Finally, step 3 covers the proper design and implemen-
tation of the TSM itself. The TSM must store cryp-
tographic keys, security policies, and secure data in its
persistent secure storage, which it protects using SP's
underlying hardware mechanisms (DRK & SRH). We
test the confidentiality and integrity of the storage itself,
plus the TSM's use of the storage and its enforcement of
the policies on accesses to the data. Adversaries might
attack the TSM's persistent data offline when stored on
disk or after the TSM has loaded it into secure memory.
Our system implements the SP hardware mechanisms,
a full TSM providing an API to the testing application,
and a suite of attacks which test both the software and
hardware components using our new testing framework.
This is a first step towards the complete validation of
the design of the SP architecture together with its ap-
plications, and provides a framework for further testing
the architecture with other software and attacks.
6 Related Work
Our testing-framework of a system architecture solution
has multiple related fields of research. Our emulation
of security architecture can be compared with hardware
simulation research, our validation mechanisms can be
compared with formal and hybrid verification method-
ologies, and our virtualization architecture can be com-
pared with systems virtualization solutions.
Micro-architectural simulators like Simplescalar  are
cycle-accurate and hence can be very useful in estimat-
ing performance metrics, but they can not simulate a re-
alistic software system with full commodity OS. Thus it
is impossible to test the security critical interactions of a
software-hardware security solution with such a simula-
tion architecture. Our emulation architecture, in using
the existing virtualization technology, enables reason-
able performance while allowing our SUT to provide
a realistic software stack. Other simulation and emu-
lation environments are available, such as Bochs ,
QEMU , and Xen . Where these environments
provide sufficient software performance and granularity
of hardware emulation, they could be used in place of
VMware to implement our framework as designed and
described in this paper.
The efforts by IBM , Intel  and others  pro-
vide the functionality of a virtual TPM device to soft-
ware, even when the physical device is not present. In
contrast, we not only emulate the new hardware but also
hook into the virtual device to observe and control its
behavior for testing purposes, and study the interaction
with other hardware and software components.
Another related area of research is the Formal Verifi-
cation of both hardware and software, in which formal
mathematics is used to write specifications for computer
hardware and software, and proof techniques are used
to determine the validity of such specifications. The
complexity of formal verification problems range from
NP-hard to undecidable [24, 25, 26, 27]. The com-
plexity of these formal verification mechanisms led to
the use of hybrid techniques  which uses some for-
mal as well as informal techniques. Some formal meth-
ods of verification are methods using theorem provers
(ACL2 , Isabelle/HOL ), model checkers, satis-
fiability solvers, etc. Some informal techniques used in
practice are control circuit exploration, directed func-
tional test generation, automatic test program genera-
tion, heuristic-based traversal, etc. The formal and hy-
brid techniques try to verify the hardware and software
separately, unlike our holistic verification of a software-
The important distinction between our approach and
these formal verification techniques is that we try to
verify the complete system while these formal tech-
niques try to verify each piece by piece. The complex-
ity of both specification and verification explodes ex-
ponentially with addition of more and more pieces to
be tested. In our approach we model both the security
critical hardware and software as a single entity, thus,
making the verification problem solvable in an informal
but systematic and efficient way.
We have designed and implemented a virtualization-
based framework for validation of new security archi-
tectures. This framework can realistically model a new
system during the design phase, and draw useful conclu-
sions about the operation of the new architecture and
Here’s what’s next.
This report can be searched. Note: Results may vary based on the legibility of text within the document.
Citing and Sharing
Basic information for referencing this web page. We also provide extended guidance on usage rights, references, copying or embedding.
Reference the current page of this Report.
Dwoskin, Jeffrey Scott, 1980-; Gomathisankaran, Mahadevan & Lee, Ruby Bei-Loh. Framework for Design Validation of Security Architectures, report, November 17, 2008; [Princeton, New Jersey]. (digital.library.unt.edu/ark:/67531/metadc130192/m1/11/: accessed May 29, 2017), University of North Texas Libraries, Digital Library, digital.library.unt.edu; crediting UNT College of Engineering.