2010 HCSS Conference Proceedings

The 10th annual HCSS Conference was held May 10-12, 2010. The program agenda and slide presentations are listed below.

2010 HCSS Conference Program Agenda

2010 HCSS Conference Program Agenda

http://cps-vo.org/node/1354

Conference Archives: 2001200220032004200520062007200820092010201120122013, 2014

Monday, May 10

8: 30 am Guardol: A Domain-Specific Language for Guards
David Hardin, Rockwell Collins
10:00 am Break
10:30 am L4.verified
Gerwin Klein, NICTA
Noon Lunch
1:30 pm Keynote Presentation: The Next IDE - Informative Development Environments
Gina Venolia, Microsoft Research
2:30 pm Break
3:00 pm Visualizing Information Flow Through C Programs
Joe Hurd, Galois
3:45 pm VAST: Visulization of Attack Surfaces for Targeting
Ke-Thia Yao, University of Southern California
4:30 pm Using Java PathFinder for Program Understanding and Defect Visualization
Peter Mehlitz, NASA Ames
5:15 pm Adjourn for the day


Tuesday, May 11

8:30 am Keynote Presentation: Alchemy: Three Ways of Transmutating Programs Into Circuits
Satnam Singh, MS Research - Cambridge, UK
9:30 am Break
10:00 am Replacing Testing with Formal Verification in Intel® Core i7™ Processor Execution Engine Validation
Roope Kaivola, Intel Corporation
10:45 am Centaur Verification Approach
Warren Hunt, University of Texas at Austin
11:30 am Lunch
1:00 pm Dean Collins, DARPA
1:45 pm Proof-Carrying Data: Secure Computation on Untrusted Execution Platforms
Eran Tromer, MIT
2:30 pm Break
3:00 pm Generating Implementations of Error Correcting Codes Using Kansas Lava
Andy Gill, University of Kansas
3:45 pm Formal Models of ARM Processors in HOL
Michael Gordon and Anthony Fox, University of Cambridge
4:30 pm HWMAC: Hardware-Enforced Fine-Grained Policy-Driven Security
Paul Karger, IBM Corporation
5:15 pm Adjourn for the day

Wednesday, May 12

8:30 am Keynote Presentation
Christopher Greer, OSTP
9:30 am Break
10:00 am Shifting the Paradigm
Ivan Sutherland, Portland State University
10:45 am Peter Lee, DARPA
11:30 am Lunch
1:00 pm Revolution Through Competition?
Carl Landwehr, NSF
1:45 pm Break
2:15 pm Helen Gill, NSF
3:00 pm Virtual Organization for Cyber-Physical Systems (CPS-VO): Goals, Plans and Actions
Janos Sztipanovits, ISIS - Vanderbilt University
3:45 pm Security Systems Engineering
Jennifer Bayuk, Stevens Institute of Technology
4:30 pm Adjourn for the day

Thursday, May 13

CAS SOFTWARE ASSURANCE WORKSHOP
8:30 am Towards Next-Generation of BitBlaze
Dawn Song, UC Berkeley
9:15 am Automated Vulnerability Injection
Dan Guinlan, Lawrence-Livermore National Labs
10:00 am Break
10:30 am CTRAD Project Briefing
Christina Smyre, Center for Assured Software, NSA
11:00 am Paul Wetzel, OPS Consulting
11:30 am Lunch
1:00 pm Moving Secure Software Assurance into Higher Education: A Roadmap for Social Change
Dan Showmaker, University of Detroit, Mercy
1:45 pm CAS Source Code Analysis Tool Testing Project
John Laliberte, Mandiant
2:30 pm Break
3:00 pm Static Analysis Tool Exposition and Reality
Paul Black, NIST
3:45 pm CAS Assurance Scoring and Validation Projects
Chuck Willis, Mandiant
4:30 pm Closing Remarks
5:15 pm Conference Adjourned

 

L4.verified

Gerwin Klein
License: 
Creative Commons 2.5

Other available formats:

L4.verified

The Next IDE: Informative Development Environment

Gina Venolia
License: 
Creative Commons 2.5

Other available formats:

The Next IDE: Informative Development Environment
Switch to experimental viewer

Visualizing Information Flow through C Programs

Joe Hurd
Aaron Tomb
David Burke
License: 
Creative Commons 2.5

Other available formats:

Visualizing Information Flow through C Programs
Switch to experimental viewer

VAST: Visualization of Attack Surface for Targeting

Ke-Thia Yao
License: 
Creative Commons 2.5

Other available formats:

VAST: Visualization of Attack Surface for Targeting
Switch to experimental viewer

Using Java PathFinder for Program Understanding and Defect Visualization

Peter Mehlitz
License: 
Creative Commons 2.5

Other available formats:

Using Java PathFinder for Program Understanding and Defect Visualization
Switch to experimental viewer

Alchemy: Three Ways of Transmutating Programs into Circuits

Satnam Singh
License: 
Creative Commons 2.5

Other available formats:

Alchemy: Three Ways of Transmutating Programs into Circuits
Switch to experimental viewer

Replacing Testing with Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation

Abstract

Formal verification of arithmetic data-paths has been part of the established methodology for most Intel processor designs over the last years. Usually formal verification has been in the role of supplementing more traditional coverage oriented testing activities. For the recent Intel(r) Core(tm) i7 design we took a step further and used formal verification as the primary validation vehicle for the core execution cluster, the component responsible for the functional behaviour of all microinstructions of the design. We applied symbolic simulation based formal verification techniques for full data-path, control and state validation for the cluster, and dropped coverage driven testing entirely. The project, involving some twenty person years of verification work, is one of the most ambitious formal verification efforts in the hardware industry to date. Our experiences show that under the right circumstances, full formal verification of a design component is a feasible, industrially viable and competitive validation approach.

Biography

Roope Kaivola is a Principal Engineer in the Converged Core Development Organization of Intel Corporation. He has worked on formal verification of Intel microprocessor component designs over the last ten years. During this time, formal verification in Intel has evolved from an untested technology giving one-off solutions to research grade problems to a mainstream engineering activity that is now routinely applied to new designs.

Roope Kaivola's area of specialization is the formal verification of arithmetic hardware. He has personally carried out formal verification of most recent Intel divider designs from Pentium 4 up to Intel Core i7, and he is the technical lead of a formal verification application group associated with a number of Intel's recent flagship processors. Prior to joining Intel in 1999, Roope Kaivola carried out academic study and research on formal verification for most of 1990's, including Ph.D. degrees in Computer Science from the University of Helsinki, Finland, and University of Edinburgh, Scotland, and a spell as a faculty member in Helsinki.

Roope Kaivola
Amber Telfer
Anna Slobodova
Armaghan Naik
Christopher Taylor
Erik Reeber
Jesse Whittemore
Naren Narasimhan
Rajnish Ghughal
Sudhindra Pandac
Vladimire Frolov
License: 
Creative Commons 2.5
Switch to experimental viewer

Centaur Verification Approach

Warren A. Hunt, Jr.
License: 
Creative Commons 2.5

Other available formats:

Centaur Verification Approach
Switch to experimental viewer

Proof-Carrying Data Secure Computation on Untrusted Execution Platforms

Eran Tromer
License: 
Creative Commons 2.5

Other available formats:

Proof-Carrying Data Secure Computation on Untrusted Execution Platforms
Switch to experimental viewer

Generating Implementations of Error Correcting Codes using Kansas Lava

Andy Gill
License: 
Creative Commons 2.5

Other available formats:

Generating Implementations of Error Correcting Codes using Kansas Lava
Switch to experimental viewer

Formal models of ARM processors in HOL

Mike Gordon
Anthony Fox
License: 
Creative Commons 2.5

Other available formats:

Formal models of ARM processors in HOL
Switch to experimental viewer

HWMAC: Hardware-Enforced Fine-Grained Policy-Driven Security

Paul Karger
License: 
Creative Commons 2.5

Other available formats:

HWMAC: Hardware-Enforced Fine-Grained Policy-Driven Security
Switch to experimental viewer

Shifting the Paradigm

Ivan Sutherland
License: 
Creative Commons 2.5

Other available formats:

Shifting the Paradigm
Switch to experimental viewer

Revolution through Competition

Carl Landwehr
License: 
Creative Commons 2.5

Other available formats:

Revolution through Competition
Switch to experimental viewer

Virtual Organization for Cyber Physical Systems (CPS-VO): Goals, Plans and Actions

Janos Sztipanovits
License: 
Creative Commons 2.5

Other available formats:

Virtual Organization for Cyber Physical Systems (CPS-VO): Goals, Plans and Actions
Switch to experimental viewer

Security Systems Engineering

Jennifer Bayuk
License: 
Creative Commons 2.5

Other available formats:

Security Systems Engineering
Switch to experimental viewer