[Colloquium] TTI-C Talk Gang Tan (2/24/05 @ 3:00 pm)

[Katherine Cumming]

TOYOTA TECHNOLOGICAL INSTITUTE TALK
 
Thursday, February 24th 3:00 pm
TTI-C Conference Room (1427 E. 60th St. - 2nd Floor) 
Refreshments provided
 
Speaker:  Gang Tan, Princeton University
Speaker's homepage: http://www.cs.princeton.edu/~gtan/
Title: Structured Verification of Unstructured Machine Code
Abstract:
Safety properties of machine code are of growing interest in both
academia and industry during recent years. Traditional Hoare Logic has
been tailored to verify properties of high-level languages with
structured control flow, but is not suitable for verifying properties of
machine code, because machine code contains goto statements with
unrestricted destinations (i.e., unstructured control flow). A
mathematical framework that modularly verifies properties of machine
code is necessary for projects such as Foundational Proof-Carrying Code
(FPCC), which produces type-safety proofs for machine code. We present a
program logic, L_c, which modularly reasons about machine-code
fragments. Unlike previous program logics, the basic reasoning units in
L_c are multiple-entry and multiple-exit code fragments. L_c provides
composition rules to combine code fragments together and to eliminate
intermediate entries/exits in the combined fragment. L_c is not only
useful for reasoning about properties of machine code with unstructured
control flow, but also useful for deriving rules for common control-flow
structures such as while-loops, repeat-until-loops, among others. We
also present a semantics for L_c and prove that L_c is both sound and
complete (with reasonable assumptions). As an application to FPCC, L_c
has been developed on top of the SPARC machine language: The semantics
of L_c is encoded in higher-order logic; its rules are proved as lemmas
with machine-checked proofs; typing rules for machine instructions in
FPCC are then derived from rules in L_c. Thus with high confidence, we
can check that the output of our certifying compiler is safe. BIO: Gang
Tan is a final-year PhD student in computer science at Princeton
University. His general research interests are in creating reliable and
secure software systems. He has done research in proof-carrying code,
runtime monitoring, safe language design and safe language
inter-operation. Gang got his B.S. from Tsinghua University in both
computer science and economics. His academic honors include a Francis
Upton Graduate Fellowship, a HSBC Bank Scholarship, and Tsinghua
University Scholarships. 
If you have questions, or would like to meet the speaker, please contact
Katherine at 4-1994 or kcumming at tti-c.org. For information on future
TTI-C talks or events, please go to the TTI-C Events
<http://ttic.uchicago.edu/events/events_dyn.php>  page. 
 
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20050217/29faf1c9/attachment.htm