In February 2024, the U.S. White House Office of the National Cyber Director (ONCD) released “Back to the Building Blocks: A Path Toward Secure and Measurable Software” [1]. The report makes the case that the technical community can greatly improve cybersecurity by moving to memory-safe languages, supported by formal methods and memory- protecting hardware, and sketches the roles that top executives, the so-called “C-suite,” play in securing software.

The SATE VI report presents the results of a security-focused bug finding evaluation exercise carried out from 2018 to 2023 on various code bases using static analysis tools. Existing bugs were extracted from bug tracker reports and the CVE/NVD database, and additional bugs were injected using automated tools and manual analysis. The results of this exercise showed significant variability across tool effectiveness, depending on the test cases, bug classes, and bug complexity involved. The report discusses the shortcomings and difficulties encountered during the bug injection process, which marginally impeded the efficiency of the evaluation. The report emphasizes the correlation between high code complexity and tool difficulty in identifying bugs. Recall and discrimination rates were lower for the convoluted C Track than the considerably less complex Java Track. Across all languages and code bases, tools found bugs with lower complexity more readily than bugs with higher complexity. Finding rates varied for different bug classes, in line with the inherent complexity of each bug class (e.g., recall for simpler initialization errors was greater than on more intricate buffer errors). The report discusses the shortcomings of the bug injection process. Regardless of the test case, injected bugs were not found by tools at the same rate as existing bugs, implying that their quality needs to improve. The report also includes a summary of the Ockham Sound Analysis Criteria track, which focused on tools that do not report false positives or false negatives. The SATE VI report concludes that static analysis is a useful technique to find real security bugs in large code bases. The right set of tools, used properly, can help increase code quality and security. Potential users should test a tool or set of tools on their own code base before using them in production. The metrics presented in SATE VI are suitable for assessing tool fitness for such a use case.

The Software Assurance Metrics and Tool Evaluation (SAMATE) team studied thousands of warnings from static analyzers. Tools have difficulty distinguishing between the absence of a weakness and the presence of a weakness that is buried in otherwise-irrelevant code elements. This paper presents classes of these code elements, which we call "code complexities." They have been present in software assurance as part of test cases generation strategy when evaluating static analyzers. Benefits of using code complexity include the development of coding guidelines, boosting diversification of test cases.

Executive Order (EO) 14028,"Improving the Nation's Cybersecurity", 12 May 2021, directs the National Institute of Standards and Technology (NIST) to recommend minimum standards for software testing within 60 days. This document describes eleven recommendations for software verification techniques as well as providing supplemental information about the techniques and references for further information. It recommends the following techniques: Threat modeling to look for design-level security issues Automated testing for consistency and to minimize human effort Static code scanning to look for top bugs Heuristic tools to look for possible hardcoded secrets Use of built-in checks and protections"Black box"test cases Code-based structural test cases Historical test cases Fuzzing Web app scanners, if applicable Address included code (libraries, packages, services) The document does not address the totality of software verification, but instead, recommends techniques that are broadly applicable and form the minimum standards. The document was developed by NIST in consultation with the National Security Agency (NSA). Additionally, we received input from numerous outside organizations through papers submitted to a NIST workshop on the Executive Order held in early June 2021, discussion at the workshop, as well as follow up with several of the submitters.

In the early days of computer science, the community settled on a simple standard model of computing and a basic canon of general purpose algorithms and data structures suited to that model. With isochronous computing, heterogeneous multiprocessors, flash memory, energy-aware computing, cache and other anisotropic memory, distributed computing, streaming environments, functional languages, graphics coprocessors, etc., the basic canon of algorithms and data structures is not enough. Software developers know of real-world constraints and new models of computation and use them to design effective algorithms and data structures. These constraints motivate the development of elegant algorithms with broad utility. As examples, we present four algorithms that were motivated by specific hardware nuances, but are generally useful: reservoir sampling, majority of a stream, B-heap, and compacting an array in $\Theta (\log n)$Θ(logn) time.

This paper examines blockchain smart contract software assurance through the lens of static analysis. Smart contracts are immutable. Once they are deployed, it is impossible to patch or redevelop the smart contracts on active chains. This paper explores specific blockchain smart contract bugs to further understand categories of vulnerabilities for bug detection prior to smart contract deployment. Specifically, this work focuses on smart contract concerns in Solidity v0.6.2 which are unchecked by static analysis tools. Solidity, influenced by C++, Python and JavaScript, is designed to target the Ethereum Virtual Machine (EVM). Many, if not all, of the warnings we categorize are currently neither integrated into Solidity static analysis tools nor earlier versions of the Solidity compiler itself. Thus, the prospective bug detection lies entirely on smart contract developers and the Solidity compiler to determine if contracts potentially qualify for bugs, concerns, issues, and vulnerabilities. We aggregate and categorize these known concerns into categories and build a model for integrating the checking of these categories into a static analysis tool engine. The static analysis engine could be employed prior to deployment to improve smart contract software assurance. Finally, we connect our fault categories with other tools to show that our introduced categories are not yet considered during static analysis.

Static analyzers examine the source or executable code of programs to find problems.Many static analyzers use heuristics or approximations to examine programs with millions of lines of code for hundreds of classes of problems.The Ockham Sound Analysis Criteria recognizes static analyzers that are precise.In brief the criteria are (1) the analyzer's findings are claimed to always be correct, (2) it produces findings for most of a program, and (3) even one incorrect finding disqualifies an analyzer.This document begins by explaining the background and requirements of the Ockham Criteria and how we determine if a tool satisfies it.As part of Static Analysis Tool Exposition (SATE) VI, we examined two tools: Astrée and Frama-C with the Evolved Value Analysis (Eva) plug-in.Examining the tool outputs led us to find several systematic mistakes in the Juliet 1.3 test suite and thousands of mistakes in its manifest of known errors.Our conclusion is that Astrée and Frama-C with Eva satisfied the SATE VI Ockham Sound Analysis Criteria.

Rising to popularity in the last decade, blockchain technology has become the preferred platform for the transfer of digital currency. Unfortunately, many of these environments are rife with vulnerabilities exploited by financially motivated attackers. Worse yet, is that a structured analysis and classification of these vulnerabilities is lacking. In this paper, we present the first formal classifications of these vulnerabilities using National Institute of Standards and Technologies Bugs (NIST’S) Framework and propose two new classes: distributed system protocol (DSP) and distributed system resource management (DRM).

We introduce opaque wrappers to prevent attackers from exploiting software bugs, but we find no way to implement them.

Statistical software" encompasses several distinct classes of software.This report explains what formal methods, tools, and approaches may be able to increase assurance of results of using statistical software and implementing differential privacy.To provide context, we present an exemplary process for assured results.The parts are data assurance, algorithm design, software production, correctness proofs, postproduction assurance of software, and result checking.We note a workshop we organized to support this paper and finish with recommended formal methods, tools, and researchers doing particularly pertinent work.

Exposure of sensitive information can be harmful on its own. In addition, it could enable further attacks. A rigorous and unambiguous definition of information exposure faults can help researchers and practitioners identify them, thus avoiding security failures. This paper describes Information Exposure (IEX), a new class in the Bugs Framework (BF). The IEX class comprises a rigorous definition and (static) attributes of the class, along with their related dynamic properties, such as proximate and secondary causes, consequences and sites. We use the IEX class to analyze specific vulnerabilities and provide clear descriptions. We also discuss lessons we learned that will help create additional BF classes.

Evaluation of scientific contributions can be done in many different ways. For the various research communities working on the verification of systems (software, hardware, or the underlying involved mechanisms), it is important to bring together the community and to compare the state of the art, in order to identify progress of and new challenges in the research area. Competitions are a suitable way to do that. The first verification competition was created in 1992 (SAT competition), shortly followed by the CASC competition in 1996. Since the year 2000, the number of dedicated verification competitions is steadily increasing. Many of these events now happen regularly, gathering researchers that would like to understand how well their research prototypes work in practice. Scientific results have to be reproducible, and powerful computers are becoming cheaper and cheaper, thus, these competitions are becoming an important means for advancing research in verification technology. TOOLympics 2019 is an event to celebrate the achievements of the various competitions, and to understand their commonalities and differences. This volume is dedicated to the presentation of the 16 competitions that joined TOOLympics as part of the celebration of the 25th anniversary of the TACAS conference.

Blockchain technology has recently emerged as the primary platform for the transfer of digital currency. This technology, which has been heralded as a revolutionary tool to facilitate the transfer of funds between participating parties, is still in its infancy and should be subjected to thorough scrutiny. In recent years, researchers have attempted to uncover a litany of bugs embedded within these distributed systems; however, there does not yet exist a formal and standardized method for their classification. In this paper, we present the first formal classifications of known bugs in smart contract systems using NIST's Bugs Framework and propose two new classes: Distributed System Protocol (DSP) and Distributed System Resource Management (DRM).

The Software Assurance Reference Dataset (SARD) is a growing collection of over 170 000 programs with precisely located bugs. The programs are in C, C++, Java, PHP, and C# and cover more than 150 classes of weaknesses, such as SQL injection, cross-site scripting (XSS), buffer overflow, and use of a broken cryptographic algorithm. Most are automatically generated synthetic programs, each a few pages of code long, but there are also over 7000 full-sized applications. In addition, SARD has production code and has hundreds of cases written by hand. The code is typical quality. It is neither pristine nor obfuscated. Many cases have corresponding “good” cases, in which weaknesses are fixed, to test for false positives.

The Juliet test suite is a systematic set of thousands of small test programs in C/C++ and Java, exhibiting over 100 classes of errors, such as buffer overflow, OS injection, hardcoded password, absolute path traversal, NULL pointer dereference, uncaught exception, deadlock, and missing release of resource. These test programs should be helpful in determining capabilities of software assurance tools, particularly static analyzers, in Unix, Microsoft Windows, and other environments. Juliet was developed by the National Security Agency’s Center for Assured Software and first released in December 2010. It has been enhanced twice since then. Version 1.2 was released in May 2013 with a total of 86 864 test cases. In the years after its release, many problems and deficiencies in Version 1.2 came to our attention. Released in October 2017, Version 1.3 fixes about fourteen systematic problems in Version 1.2 and adds tests for prefix and postfix increment integer overflow and decrement integer underflow. This technical note details the changes from Version 1.2 to 1.3. This note also lists known problems remaining in Juliet 1.3.

Random number generators may have weaknesses (bugs) and the applications using them may become vulnerable to attacks. Formalization of randomness bugs would help researchers and practitioners identify them and avoid security failures. The Bugs Framework (BF) comprises rigorous definitions and (static) attributes of bug classes, along with their related dynamic properties, such as proximate and secondary causes, consequences and sites. This paper presents two new BF classes: True-Random Number Bugs (TRN) and Pseudo-Random Number Bugs (PRN). We analyze particular vulnerabilities and use these classes to provide clear BF descriptions. Finally, we discuss the lessons learned towards creating new BF class.

The Software Assurance Metrics and Tool Evaluation (SAMATE) team studied thousands of warnings from static analyzers. Tools have difficulty distinguishing between the absence of a weakness and the presence of a weakness that is buried in otherwise-irrelevant code elements. This paper presents classes of these code elements, which we call “code complexities.” They have been present in software assurance as part of test cases generation strategy when evaluating static analyzers. Benefits of using code complexity include the development of coding guidelines, boosting diversification of test cases.