The Twenty-Third Annual

High Confidence Software and Systems (HCSS) Conference

CALL FOR PRESENTATIONS

OVERVIEW

The twenty-third annual High Confidence Software and Systems (HCSS) Conference will be held May 8-10, 2023 at the Historic Inns of Annapolis in Annapolis, Maryland. We solicit proposals to present talks at the conference. 

IMPORTANT DATES

• CfP Abstracts Due: January 13, 2023 extended to January 24, 2023
• Notification of Decisions: February 17, 2023
• HCSS Conference: Week of May 8-10, 2023

BACKGROUND

Our security, safety, privacy, and well-being increasingly depend upon the correctness, reliability, resilience, and integrity of software-intensive systems of all kinds, including cyber-physical systems (CPS). These systems must be capable of interacting correctly, safely, and securely with humans, with diverse other systems, and with the physical world even as they operate in changing, difficult-to-predict, and possibly malicious environments. New foundations in science, technology, and methodologies continue to be needed. Moreover, these methods and tools have to be transitioned into mainstream use to build and assure these systems—and to move towards more effective models for acceptance and certification.

CONFERENCE SCOPE, GOALS, AND VISION

The High Confidence Software and Systems (HCSS) Conference draws together researchers, practitioners, and management leaders from government, universities, non-profits, and industry. The conference provides a forum for dialogue centered upon the development of scientific foundations for the assured engineering of software-intensive complex computing systems and the transition of science into practice. The technical emphasis of the HCSS conference is on mathematically-based tools and techniques, scientific foundations supporting evidence creation, systems assurance, and security. The HCSS vision is one of engaging and growing a community—including researchers and skilled practitioners—that is focused around the creation of dependable systems that are capable, efficient, and responsive; that can work in dangerous or inaccessible environments; that can support large-scale, distributed coordination; that augment human capabilities; that can advance the mission of national security; and that enhance quality of life, safety, and security.

CONFERENCE THEMES

We invite submissions on any topic related to high-confidence software and systems that aligns with the conference scope and goals listed above. In addition, the 2023 HCSS Conference will highlight the following themes:

Open Source

The last few years have seen the emergence of a new type of open-source exploit. In addition to the typical approach of looking for existing vulnerabilities in open-source software, attackers are increasingly creating their own opportunities by becoming trusted contributors and injecting malicious code or adding insecure dependencies. These types of attacks have increased dramatically in recent years. This development increases the importance of a variety of formal methods topics. Specifications become more important when we can't trust the intent of code contributions. Malicious code detection becomes more critical and requires a new level of scale when all 3 million+ open-source projects are at risk. And issues of trust, provenance, and software integrity take center stage when the entire software development pipeline may be subject to attack.

In this topic, we welcome all contributions that relate to securing open-source software and the software development process, to include:

• Enhancements of engineering and development tooling to encompass models, analyses, argumentation structures, and other evidence to support concurrent evolution of system artifacts, associated models, and supporting security / quality analyses.
• Models of trust and risk to evaluate the trustworthiness of a component given its supply chain and development process.
• Attestation and formal auditing technology to certify analysis results and prevent tampering within the development pipeline.
• Certified analysis tooling and proof checking technology to ensure that the results of formal tools are trustworthy (note that many formal tool chains and high performance solvers are themselves open source and thus open to open-source supply chain attacks).
• Support for automated analysis of components and services to identify potential vulnerabilities and other weaknesses. 
• Automation to support rapid and confident repair for open-source components.
• Architectural and design fragment models for library and framework APIs, that build in security and resiliency.

Protocol Verification

Protocols arise in system designs whenever multiple actors need to communicate in order to coordinate, such as synchronizing clocks, establishing shared secrets in cryptographic systems, or ensuring coherency of caches. Protocols may exhibit unforeseen vulnerabilities to accidental or malicious duplication of messages, manipulation of data by an entity-in-the-middle, and resource exhaustion.  Understanding properties of protocols is difficult for people, as properties that a single protocol instance establishes can sometimes be violated by composing multiple instances of the same protocol, and protocol states in many distributed instances can become unboundedly complex, with subtle reliance on freshness, privacy, security, and authenticity properties.   It is essential that the composition of these elements into full protocols maintains key properties, both of the implementation and behavior of underlying state machines.

The theme of Protocol Verification will explore:

• The verification of protocol specifications (verifying that a protocol’s design upholds certain properties such as liveness, confidentiality, integrity, and authenticity)
• The verification of implementations (verifying that the code correctly implements the specification). 
• The validation of assumptions made in the verifications above about environments (such as system-of-systems architectures, environmental concerns, and threat models including adversarial actions)

Verification of protocol specifications is quite a mature area with widely-used tools such as Tamarin, ProVerif, and CPSA, but bridging the gap between these abstract (often symbolic) specifications and real world implementations is a substantial open research challenge, where expertise from the HCSS community may well be a strong area for collaboration.

Proof of Bugs

The canonical application of formal verification is to prove systems correct. But they can also be leveraged for proof of incorrectness, to show when a system has a bug, vulnerability, or exploit. For example, a counterexample to a theorem may be a proof that a corresponding bug exists in the modeled system. In this theme, we solicit research and case-studies related to applying formal techniques to discovering bugs. This includes logics and reasoning techniques for discovering bugs as well as how to map formal models to actual issues. Example topics include but are not limited to: 

• Applications of formal methods for bug hunting.
• Applications of formal methods for counterexample generation and explanation.
• Applications of formal methods for exploit generation.
• Combinations of bug finding and verification, allowing proof engineering that is more pay-as-you-go, where there is a pathway to incremental assurance of a system.
• Explainability/compactness in SAT/SMT counterexamples.
• Explorations of incorrectness logic on enabling compositional bug finding, where potential bugs or vulnerabilities can be broken into 'sub-bugs', which are analyzed separately.
• Mapping proofs of incorrectness to system bugs.
• Applications of formal methods to analysis and verification of system requirements.
• Proof of incorrectness in system assumptions.
• Design and architectural flaws that impair correctness and resiliency.

Semantically Rigorous and Integrated High-Level Abstractions

High-level abstractions play a key role in model-based development (MBD) approaches.  Due to past successes of MBD, the US Department of Defense vision for future system development, as presented by its Digital Engineering Strategy (DES), encourages models to be "formally developed" and applied to inform enterprise and program decision making.  This vision emphasizes the need for "an enduring, authoritative source of truth" to enable infrastructure and development environments and to support collaborating and communication across stakeholders. At lower levels of abstraction, the formal methods community has made significant progress on developing robust approaches, tools, and infrastructure that are now being adopted in industry.  This includes techniques for specifying semantics (e.g., mechanized operational, axiomatic, and denotational semantics), theories of composition with automated verification (e.g., code-level contracts), high-confidence translation and compilation (e.g., verified compilers), high-assurance platforms (e.g., verified micro-kernels), and semantically sound analyses (e.g., powerful proven-correct type systems and a plethora of semantically-grounded static analyses).  However, the same levels of breadth, maturity, and industrial transition are not being achieved at higher levels of abstraction, and providing an "enduring authoritative source of truth" at the model level still seems like a distant goal.

For this theme, HCSS seeks contributions that build on successes at lower levels of abstraction to provide usable semantically-rigorous high-level abstractions that can be integrated directly into industrial workflows.  Potential topics include:

• Leverage-able formal semantics for technical architecture modeling languages.
• Developer-friendly tool-support approaches for model-based compositional reasoning
• Semantically-grounded frameworks for model-to-model transformations and model-to-code generation, as well as model-based analyses

Of particular interest are approaches that integrate previous work on verified infrastructure (micro-kernels, communication substrates), programming language technology, and platform elements to help the community form a vision for end-to-end, formally-supported, model-based development.

CONFERENCE PRESENTATIONS

The conference program features invited speakers, panel discussions, poster presentations, and a technical track of contributed talks.

Technical Track Presentations

The technical track features two kinds of talks:

·   Experience reports. These talks inform participants about how emerging HCSS and CPS techniques play out in real-world applications, focusing especially on lessons learned and insights gained. Although experience reports do not have to be highly technical, they should emphasize substantive and comprehensive reflection, building on data and direct experience. Experience reports focus on topics such as transitioning science into practice, architecture and requirements, use of advanced languages and tools, evaluation and assessment, team practice and tooling, supply-chain issues, etc.

·   Technical talks. These talks highlight state-of-the-art techniques and methods for high-confidence software systems with an emphasis on how those techniques and methods can be used in practice. Presenters of these talks should strive to make their material accessible to the broader HCSS community even as they discuss deep technical results in areas as diverse as concurrency analysis, hybrid reasoning approaches, theorem proving, separation logic, synthesis, analytics, various modeling techniques, etc.

If you are interested in offering a talk—or nominating someone else to be invited to do so—please upload an abstract of one page or less for your proposed talk or a one paragraph description of your nominee’s proposed talk by January 13, 2023 January 24, 2023 to https://archive.cps-vo.org/hcss-2023/cfp. Abstracts and nomination paragraphs should clearly indicate why the talk would be relevant to HCSS and which, if any, conference themes the talk would address. Notifications of accepted presentations will be made by February 10, 2023. 

Further instructions for electronically submitting print-ready abstracts and final slide presentations will be provided in the acceptance notification messages. Abstracts of accepted presentations will be published on the HCSS Conference website.

Co-Located Meetings

We are pleased to announce the co-location of the Trusted Computing Center of Excellence™ (TCCoE). The mission of the TCCoE is to lower barriers to adoption and facilitate the principled development and deployment of trustworthy systems. The TCCoE, originally focused on facilitating the adoption of the seL4 kernel in critical defense systems. Recently, the TCCoE has broadened their mission  to promote the adoption and deployment of formally verified software (including seL4)  in defense applications whose mission requires the highest levels in assurance. The annual TCCoE Summit brings together like-minded individuals from Government, Industry, and Academia to learn of relevant developments, make connections, and work toward the TCCoE’s goals. This year’s summit will leverage synergies with the High Confidence Software and Systems Conference. The overlap between the technologies of interest of these two events and their complementary missions will provide interested attendees a tremendous experience. The TCCoE Summit will be held on May 11-12, 2023.

The Software Certification Consortium (SCC) meeting will again be co-located with HCSS. The meeting will run concurrently to the TCCoE Summit on May 11-12, 2023. The Software Certification Consortium is a group of researchers/practitioners who are interested in the development and certification of high integrity systems. SCC typically meets twice a year, and the themes of the meetings are designed to contribute to a long-term SCC work plan. Information about the previous meetings can be found at https://archive.cps-vo.org/group/scc.

ADDITIONAL INFORMATION

Instructions for submitting print-ready abstracts and final slide presentations will be provided for accepted talks. Abstracts of accepted presentations will be posted on the conference website.

IMPORTANT DATES

CfP Abstracts Due: January 13, 2023 January 24, 2023
Notification of Decisions: February 17, 2023
Camera-Ready Abstracts Due: March 17, 2023
Slides Due: May 7, 2023
HCSS Conference: May 8-10, 2023

Co-located Meetings
TCCOE Summit: May 11-12, 2023
SCC Meeting: May 11-12, 2023

PLANNING COMMITTEE

Co-Chairs

Patrick Lincoln, SRI International
Kristin Yvonne Rozier, Iowa State University

Steering Group

Perry Alexander, University of Kansas
June Andronick, Proofcraft
Kathleen Fisher, DARPA
John Hatcliff, Kansas State University
John Launchbury, Galois, Inc.
Stephen Magill, Sonatype
Brad Martin, DARPA
Martin, NCSC
Lee Pike, Amazon Web Services
Ray Richards, Leidos
Bill Scherlis, Carnegie Mellon University
Eric Smith, Kestrel Institute
Sean Weaver, National Security Agency
Matt Wilding, DARPA

Organizers

Katie Dey, Vanderbilt University
Regan Williams, Vanderbilt University

Sponsor Agency

NITRD HCSS Coordinating Group