Program

Welcome & Opening Remarks
HCSS Chairs:
Patrick Lincoln (SRI International)
Kristin Yvonne Rozier (Iowa State University)

0900 - 1000

Keynote: Tomorrow’s Shared-Everything Architectures
Josh Fryman (Intel)

1000 - 1030

BREAK

1030 - 1100

A Framework for Assuring Increasingly Autonomous Systems in Human-Machine Teams
Jennifer Davis (Collins Aerospace)

1100 - 1130

MAESTRO: Measurement and Attestation Execution and Synthesis Toolkit for Remote Orchestration
Adam Petz (University of Kansas (I2S))

1130 - 1200

Tools for Assurance-based Learning-enabled Cyber-Physical Systems: An Experience Report
Gabor Karsai (Vanderbilt University)

1200 - 1330

LUNCH (on your own)

1330 - 1400

Next Steps for Trustworthy Machine Learning
Darren Cofer (Collins Aerospace)

1400 - 1430

Semantic Backplane for Model-Based Development
Daniel Balasubramanian (Vanderbilt University)

1430 - 1500

Proteus: Automated Cyber Reasoning
Bill Bierman (GrammaTech, Inc)

1500 - 1530

POSTER SESSION / BREAK

1530 - 1600

Oqarina – Mechanization of the AADL Architectural Description Language
Jerome Hugues (CMU/SEI)

1600 - 1630

Leverageable Semantics Definitions and Contract Reasoning for a Technical Architecture Description Language
John Hatcliff (Kansas State University)

1630 - 1700

Signet-ring: A Framework for Authenticating Sources and Lineages of Digital Objects
Mahesh Arumugam and Catherine Jimerson (UC Berkeley)

1700

Adjourn for the day

0900 - 1000

Keynote: Making sense of Cyber's Why, What, How and Who
A discussion of a whole of nation approach to ensuring cyberspace meets our needs.
Chris Inglis (Former U.S. National Cyber Director)

1000 - 1030

BREAK

1030 - 1100

Grading Open Source Software Development Practices
Stephen Magill (Sonatype, Inc.)

1100 - 1130

CRAM: C++ to Rust Assisted Migration
Thomas Wahl (Gramma Tech)

1130 - 1200

Bridging the Gap between Protocol Specification and Program Verification
Alexander Senier (AdaCore)

1200 - 1330

LUNCH (on your own)

1330 - 1430

Keynote: From C to Rust: a Software Verification Journey
Jonathan Protzenko (Microsoft Research)

1430 - 1500

Formal Verification of Security and Privacy Requirements in Modern ICT
Systems Assisted by the Tamarin Security-protocol Prover
Ioana Boureanu (University of Surrey, Surrey Centre for Cyber Security)

1500 - 1530

POSTER SESSION / BREAK

1530 - 1600

Secure Device Design via Protocol Analysis
Joshua Guttman (The MITRE Corporation)

1600 - 1630

Reasoning about the Robustness of Protocols
Eunsuk Kang (Carnegie Mellon University)

1630 - 1700

Zappa for Correctly Implementing CPSA Analyzed Protocols
John Ramsdell (The MITRE Corporation)

1630

Adjourn for the day

0900 - 1000

Keynote: Underapproximate Reasoning at Scale
Peter O'Hearn (Lacework and University College London)

1000 - 1030

BREAK

1030 - 1100

Incorrectness Logic for Scalable Bug Detection
Azalea Raad (Imperial College London)

1100 - 1130

Cheesecloth: Zero-Knowledge Proofs of Real-World Vulnerabilities
James Parker (Galois, Inc)

1130 - 1200

A Unified View of Weirdness: A Logical Framework for Emergent Execution
William Harrison (Two Six Technologies)

1200 - 1330

LUNCH (on your own)

1330 - 1400

Synergizing Model-based and Data-driven Methods for CPS Design
Sandeep Neema, Vanderbilt University

1400 - 1430

Scalable and Provable Distributed SAT Solving
Michael Whalen (Amazon Inc. and The University of Minnesota)

1430 - 1500

Verification-Guided Development of the Cedar Authorization Language
Kesha Hietala (Amazon Web Services (AWS))

1500 - 1530

POSTER SESSION / BREAK

1530 - 1600

Capabilities Labeling
Greg Nelson (GrammaTech Inc.)

1600 - 1630

Zelkova: A Billion SMT Queries a Day
Jeremiah Dunham (Amazon Web Services)

1630 - 1700

TCCoE Introduction
HCSS Closing Remarks

1700

Adjourn for the day

CONFERENCE ADJOURNED