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.

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).

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 $$25^{ th }$$ anniversary of the TACAS conference.

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.

To achieve higher levels of assurance for digital systems, we need to answer questions such as does this software have bugs of these critical classes? Do two software assurance tools find the same set of bugs or different, complimentary sets? Can we guarantee that a new technique discovers all problems of this type? To answer such questions, we need a vastly improved way to describe classes of vulnerabilities and chains of failures. We present the Bugs Framework (BF), which raises the current realm of best efforts and useful heuristics. Our BF includes rigorous definitions and (static) attributes of bug classes, along with their related dynamic properties, such as proximate, secondary and tertiary causes, consequences and sites. The paper discusses the buffer overflow class, the injection class and the control of interaction frequency class, and provides examples of applying our BF taxonomy to describe particular vulnerabilities.

Software Assurance Metrics and Tool Evaluation (SAMATE) is a broad, inclusive project at the U.S. National Institute of Standards and Technology (NIST) with the goal of improving software assurance by developing materials, specifications, and methods to test tools and techniques and measure their effectiveness. We review some SAMATE sub-projects: web application security scanners, malware research protocol, electronic voting systems, the SAMATE Reference Dataset, a public repository of thousands of example programs with known weaknesses, and the Static Analysis Tool Exposition (SATE). Along the way we list over two dozen possible research questions, which are also collaboration opportunities. Software metrics are incomplete without metrics of what is variously called bugs, flaws, or faults. We detail numerous critical research problems related to such metrics. For instance, is a warning from a source code scanner a real bug, a false positive, or something else? If a numeric overflow leads to buffer overflow, which leads to command injection, what is the error? How many bugs are there if two sources call two sinks: 1, 2, or 4? Where is a missing feature? We conclude with a list of concepts which may be a useful basis of bug metrics.

Software development, testing, and maintenance tools must yield assurance information in a standardized form. Developers can use this information to argue that the software is adequate for its use and secure enough for the risk. NIST's Software Assurance Metrics And Tool Evaluation (SAMATE) project is developing specifications for software assurance tools. These specifications can include optional features for assurance information reports, encouraging tools to provide them. During maintenance, developers can collect this information to make explicit assurance cases

The purpose of the workshop is to convene researchers, developers, and government and industrial users of software security assurance (SSA) tools to refine the taxonomy of flaws and the taxonomy of SSA tool functions, converge on which SSA functions should first have specifications and tests developed, gather SSA tool developers for "target practice" on the reference datasets, and identify gaps or requirements for research in SSA functions. There are contributions describing basic research, novel applications, and experience relevant to SSA tools and their evaluation. The reference datasets are code with known flaws and vulnerabilities, with corresponding correct versions, to be used as references for tool testing, to make research easier, and to be a standard of evaluation. Tools ranging from commercial products to university projects "shoot holes" in the datasets to suggest extensions, improvements, etc. This is a U.S. National Institute of Standards and Technology SAMATE (http://samate.nist.gov/) workshop.

Testing has a vital support role in the software engineering process, but developing tests often takes significant resources. A formal specification is a repository of knowledge about a system, and a recent method uses such specifications to automatically generate complete test suites via mutation analysis. We define an extensive set of mutation operators for use with this method. We report the results of our theoretical and experimental investigation of the relationships between the classes of faults detected by the various operators. Finally, we recommend sets of mutation operators which yield good test coverage at a reduced cost compared to using all proposed operators.

A conformance test is a software assurance test that is applied in order to determine if specification requirements of the software are being met. It is a time-independent model, where the software object is subjected to an a priori known test suite. The reliability of the software is the probability that it will function properly for values in the input space. Because the input space is usually very large, it is impossible to sample all input values, so in order to provide better sampling coverage, the input space is partitioned into homogeneous subspaces. Samples are drawn from each subspace for testing the software. The conformance tests based on these samples are required to pass all tests in the test suite. Based on these data, the classical statistical estimate of reliability is one. Such an estimate may be unrealistic if the sample sizes are not large. Even in such a scenario a nontrivial confidence interval is provided for the reliability.

We apply a model checker to the problem of test generation using a new application of mutation analysis. We define syntactic operators, each of which produces a slight variation on a given model. The operators define a form of mutation analysis at the level of the model checker specification. A model checker generates countersamples which distinguish the variations from the original specification. The countersamples can easily be turned into complete test cases, that is, with inputs and expected results. We define two classes of operators: those that produce test cases from which a correct implementation must differ, and those that produce test cases with which it must agree. There are substantial advantages to combining a model checker with mutation analysis. First, test case generation is automatic; each countersample is a complete test case. Second, in sharp contrast to program-based mutation analysis, equivalent mutant identification is also automatic. We apply our method to an example specification and evaluate the resulting test sets with coverage metrics on a Java implementation.