The Twenty-Fourth High Confidence Software and Systems (HCSS) Conference
May 6-8, 2024 | Annapolis Maryland
Introduction
The twenty-fourth annual High Confidence Software and Systems (HCSS) Conference will be held May 6-8, 2024 at the Historic Inns of Annapolis in Annapolis, Maryland. We solicit proposals to present talks at the conference.
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 2024 HCSS Conference will highlight the following themes:
Assured Open Source and Memory Safety
The scale and impact of the open-source ecosystem is huge. Examples include the Linux operating system (with 21K developers for the kernel alone), the NPM web apps ecosystem (with nearly 1M components), the Apache family (the most widely used web server infrastructure), and Mozilla (Firefox browser, Thunderbird email). The bias toward reliance on fully open-source supply chains is important for several reasons – for example, it enables developers to adapt their own tooling (also open source) in order to address an immediate challenge, with the effect that tools are continually improved and so routine processes become increasingly automated over time, with consequent ramp-ups in productivity and affordability. The most successful open-source projects operate as de facto consortia, where stakeholders or their proxies jointly participate in repairs and enhancements, and in a manner that is transparent to participants. Transparency within open-source ecosystems enables data-intensive automation in engineering, and also the potential for more aggressive approaches to assurance.
Ensuring memory safety in software is widely recognized as an effective means of eliminating a large class of vulnerabilities. While memory safety properties can be demonstrated through analysis, the use of modern memory safe languages in development can provide effective proof of the desired memory safety. Despite this clear benefit, languages such as Rust or Go have only seen limited adoption. Moreover, large amounts of legacy code were developed without the benefits of memory safe techniques. Moving forward, memory safe languages need to be positioned for broader adoption (perhaps the adoption of standards) and approaches need to be developed to provide the benefits of memory safety to existing software.
Recognizing the benefits and risks of the open-source ecosystem, the Office of the National Cyber Director (ONCD) outlined its commitment within the National Cybersecurity Strategy Implementation Plan (July 2023) to invest in the development of open-source software security and the adoption of memory safe programming languages. Building on that commitment ONCD announced (August 2023) a Request For Information on open source software security and memory safe programming languages.
Building upon discussions from HCSS ’23 which centered on securing open-source software and the software development process, the focus of this HCSS ’24 theme is to explore evidence, languages, tooling, and practices within the context of the rapid pace of open-source project evolution, to include:
- The kinds of evidence, languages, hardware, and tooling that could contribute to significant open-source projects,
- The means to integrate evidence, languages, and tooling, including both integration directly into build infrastructure and, additionally, a "standoff" model whereby evidence, languages, and tooling would be separately managed (but with consistency maintenance) from the open-source repo and tool chains,
- Case studies with particular open-source libraries and components, and
- Techniques whereby assurance evidence can be incrementally introduced, to avoid the risks of "all at once" integrations.
Program Transformations
Modern software manipulation techniques such as API refactoring, program generation, bug repair, and weird machine implementation are often framed as program transformations. A benefit of this framing is that expressing informal techniques for program manipulation as formal transformations should enable them to be more easily mechanized and reasoned about. The history of this framing goes back more than fifty years, with the early development of expressive meaning-preserving transformations designed for code optimization, algorithm design, and program specialization using techniques such as partial evaluation. In the 1990s there was renewed focus under the flag of refactoring, with transformations that were less structurally ambitious but arguably more realistic with regard to modern languages and software at scale. More recently, transformational techniques are receiving attention in contexts including automated defect repair and other kinds of automatic program improvement.
We welcome contributions that relate to these topics and applications, such as:
- Transformation techniques for common software tasks such as algorithm enhancement, security enhancement, API adaptation, tailoring to hardware architectures, performance enhancement, etc.
- Techniques focused on more ambitious tasks such as support for creation of capabilities for dynamic adaptation, implementation of resilient response, algorithm improvement, and adaptation for runtime auditing and logging.
- Transformations in the context of domain-specific languages and generation, including ways to reduce the need to adapt generated code.
- Techniques to express and reason about transformations, including those that preserve meanings, such as for optimization or refactoring, and those that change meanings, such as for defect repair or enhancing resiliency.
Use of Large Language Models in High-Assurance Contexts
Large language models (LLMs) have rapidly expanded in scale and capability. Unfortunately, there are still many deficiencies in LLM performance in high-consequence contexts, with problems including hallucination, bias, emphasis on artificial data or outdated data, high latency, and misalignment. High-consequence uses of LLMs demand high-assurance, which may be achievable through a combination of approaches. Two such approaches are finding specific patterns of use of LLMs where the machine learning system produces efficient arguments (i.e., evidence that can be efficiently checked by relatively simple systems), and generative techniques to produce specifications – perhaps specifications that are generated from externally visible actions of relatively opaque systems.
LLM deficiencies include:
- Hallucination: LLMs sometimes generate seemingly-coherent but inaccurate or completely made-up information. Mitigating the risks of hallucination may involve detecting and mitigating misleading or false outputs, through model-based post-processing, cross checking, and other means.
- Bias: LLMs trained on a massive corpus of human-generated data (social media feeds, etc) may inadvertently absorb those biases and perpetuate them in their outputs. Methods to mitigate inherent bias in learned systems include enforcement of curation of inclusive and representative datasets, governance mechanisms to continuously monitor and audit LLM outputs.
- Detection of and reliance on artificial data: LLMs rely on unmarked training data, some of which may be machine generated. For example, one LLM may post (possibly wrong) answers on stack overflow, which are then used by other LLMs to train on, leading to a spiral or “toxic spill” of wrong information that leads to more and more wrong information in the future. Also, some LLMs are able to produce outputs that are indistinguishable by normal human users from human-generated outputs. Detecting artificial or manipulated data is thus an important issue.
- Use of outdated data: LLMs are trained on available datasets, which may contain old data that is superseded or corrected by newer updated data. Unfortunately, LLMs do not track data provenance nor have native means to retract specific data inputs. Methods like model editing, retrieval augmentation, and watermarking attempt to address this.
- High latencies and other costs: LLMs can suffer from slow inference due to low parallelizability (inherent sequential nature of some portion of inference computation), memory bandwidth demands, and poor scaling in attention mechanisms. Methods based on new inference techniques such as forward-forward may reduce latency, but may increase power use.
- Misalignment: The alignment problem of LLMs includes producing outputs at odds with the intents and designs of the builders, owners, and operators, sometimes accidentally and sometimes as a result of “jailbreaking” malicious activities of users. Approaches to address the issue are in their infancy and include fine-tuning with specific constrained examples, and training with human feedback may address some portion of the problem.
Approaches of specific interest to HCSS include:
- Finding patterns of use, prompt engineering, and infrastructure to cause production of efficient arguments. Efficient arguments are types of evidence that can be efficiently checked by a relatively simple system. For example, a claim of satisfiability of a Boolean formula, can be efficiently checked by a simple circuit evaluator based on a given specific mapping of Boolean variables mapped to true and false. Such efficient arguments may be exponentially faster and cheaper to check than to produce.
- Generative techniques may be trained and fine-tuned to produce machine-friendly specifications. Specifications can be difficult for humans to write or check without automated support. Symbolic techniques can be used to check if a specification is consistent or complete. Partial or missing specifications can be inferred from externally-observable behavior, even for black-box or partially opaque systems, sometimes starting with human-defined structure and general goals of the specification, refined and checked by automated methods.
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, 2024 extended to January 20, 2024 to https://sos-vo.org/group/hcss_conference/cfp/2024-submit. 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 17, 2024.
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 once again welcome the co-location of the Trusted Computing Center of Excellence™ (TCCoE) Summit. 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 9-10, 2024.
The Software Certification Consortium (SCC) meeting will again be co-located with HCSS. The meeting will run concurrently to the TCCoE Summit on May 9-10, 2024. 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.
Important Dates
- CfP Abstracts Due: January 13, 2024 extended to January 20, 2024
- Notification of Decisions: February 17, 2024
- HCSS Conference: May 6-8, 2024
Co-located Meetings
- TCCOE Summit: May 9-10, 2024
- SCC Meeting: May 9-10, 2024
Planning Committee
Co-Chairs
- Darren Cofer, Collins Aerospace
- 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.
- Patrick Lincoln, SRI International
- Stephen Magill, Sonatype
- Brad Martin, DARPA
- 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
Organizer
Katie Dey, Vanderbilt University
Sponsor Agency
NITRD HCSS Coordinating Group