The goal of this research is to continue the development of a comprehensive approach to software safety and to evaluate the approach with a case study. The case study is a major part of the project, and it involves the analysis of a specific safety-critical system from the medical equipment domain. The particular application being used was selected because of the availability of a suitable candidate system. We consider the results to be generally applicable and in no way particularly limited by the domain. The research is concentrating on issues raised by the specification and verification phases of the software lifecycle since they are central to our previously-developed rigorous definitions of software safety. The theoretical research is based on our framework of definitions for software safety. In the area of specification, the main topics being investigated are the development of techniques for building system fault trees that correctly incorporate software issues and the development of rigorous techniques for the preparation of software safety specifications. The research results are documented. Another area of theoretical investigation is the development of verification methods tailored to the characteristics of safety requirements. Verification of the correct implementation of the safety specification is central to the goal of establishing safe software. The empirical component of this research is focusing on a case study in order to provide detailed characterizations of the issues as they appear in practice, and to provide a testbed for the evaluation of various existing and new theoretical results, tools, and techniques. The Magnetic Stereotaxis System is summarized.

Real-world applications often include large, empirically defined discrete-valued functions. When proving properties about these applications, the proof naturally breaks into one case per entry in the first function reached, and again into one case per entry in the next function, and continues splitting. This splitting yields a combinatorial explosion of proof cases that challenges traditional proof approaches. While each proof case represents a mathematical path from inputs to outputs through these functions, the full set of cases is not available up front, preventing a straightforward application of parallelism. Here we describe an approach that slices the input space, creating a partition based on pre-computed mathematical paths such that each slice has only a small number of proof cases. These slices are amenable to massively parallel proof. We evaluate this approach using an example model of an adaptive cruise control, where proofs are conducted in a highly parallel PVS environment.

The actions taken by software should be consistent with relevant constraints arising in the real world. For example, computations should not mix values that are understood as being expressed in incompatible physical units. To enable checking of such consistency our previous work introduced: (a) a new structure, the interpreted formalism, that is a software analog of the notion of an informal interpretation from classical logic, and (b) a practical implementation of the concept in the form of real-world type systems. We reported preliminary results of the value of interpreted formalisms in improving software dependability. In this paper, we present details of a new case study, the results of which indicate that: (a) interpreted formalisms can be applied to large systems, and (b) the fault-detection potential is substantial.

Modern cyber-physical systems place ever-increasing reliance on high-assurance software. Recent high-profile safety and security incidents directly attributable to software point to a failure to develop sufficient assurance of software correctness through verification and validation. While formal methods provide techniques for proving that critical safety and security properties hold for all inputs and all execution paths, engineers typically rely on simulation and testing -- which can only establish the presence but not the absence of defects. A key reason for the lack of application of formal methods is the perception that they are difficult to learn and to use. In previous work, we introduced Simulink2PVS, a tool that converts SIMULINK models to the PVS specification language. In this paper, we extend Simulink2PVS to translate the checks associated with SIMULINK assertion blocks to putative theorems. This approach allows engineers to state critical safety and security properties using SIMULINK assertion blocks, which are immediately familiar to engineers with SIMULINK experience. Engineers can then prove that the properties hold for all inputs and all execution paths. As a result, the expressive and analytic power of the engineer's existing toolkit has been greatly increased and engineers are able to greatly enhance their confidence in the assurance provided by the software.

In this paper, we argue that standards, especially those intended to support critical applications, should define explicitly both the properties expected to accrue from use of the standard and an explicit rationale that justifies the contents of the standard. Current standards do not include an explicit, comprehensive rationale. Without a rationale, the use, maintenance, and revision of standards is unnecessarily difficult. We introduce a new concept for standards, the rationalized standard. A rationalized standard combines: (a) an explicit goal defining a property desired for conformant systems, (b) guidance that, if followed correctly, should yield an entity with the property stated in the goal, and (c) the rationale showing the reasoning why there is assurance with reasonable confidence that a conformant entity will have the property defined by the goal. We illustrate the utility of an explicit rationale using an existing safety standard, ISO 26262.

Establishing properties of binary programs by proof is a desirable goal when the properties of interest are crucial, such as those that arise in safety- and security-critical applications. Practical development of proofs for binary programs requires a substantial infrastructure to disassemble the program, define the machine semantics, and actually undertake the required proofs. At the center of these infrastructure requirements is the need to document semantics in a formal language. In this paper we present a work-in-progress proof infrastructure for binary programs based on AdaCore and Altran’s integrated development and verification environment, SPARKPro. We illustrate the infrastructure with proof of a security property.

Cytotoxic constituents of the terrestrial plant Bridelia ferruginea were isolated using bioactivity-guided fractionation, which revealed the presence of the previously known deoxypodophyllotoxin (1), isopicrodeoxypodophyllotoxin (2), β-peltatin (3), β-peltatin-5-O-β-D-glucopyranoside (3a), and the indole neoechinulin (4). As an extension of previous podophyllotoxin research, SAR studies were undertaken focused on 4-aza-podophyllotoxin structural modifications. A number of such derivatives were synthesized following modifications to the A and E rings. Such structural modifications with alkyl and 4-fluorobenzyl substituents at the 4-aza position provided the most potent cancer cell growth inhibitory activity (GI50 0.1 to <0.03 μg/mL) against a panel of six human cancer cell lines and one murine cancer cell line. Several compounds corresponding to 4'-demethylated modifications were also synthesized and found to be significantly less potent.

Randomizing software characteristics can help thwart cyberattacks by denying critical information about a target system previously known to an attacker.

Software for which development artifacts are missing is increasingly common and difficult to avoid, including in embedded systems. The lack of development artifacts leaves doubt about whether the software possesses critical security properties and makes enhancement of the software extremely difficult. Embedded systems often have strict resource restrictions/constraints making the application of security enhancements especially difficult. In this paper, we present details of a system that is being developed to provide significant protection against security exploits of embedded systems. The system operates on binary programs. No source code or other development artifacts are required, and the typical size and time constraints of embedded systems are accounted for in the analysis and processing of subject binary programs. Formal verification of security properties is used to eliminate unnecessary security transformations, and transformations are applied by a highly efficient static binary rewriter.

No abstract available.

This paper explores domain arguments-arguments about why techniques, processes, and designs possess properties as believed by their domain experts. An elicitation technique for their recovery from domain documents is presented. This is followed by demonstrated application of the technique to several domain artifacts from aviation engineering. The elicited arguments are presented and analyzed for their properties. The inherent importance of such arguments is discussed as well as their potential contribution to system assurance arguments such as the safety case.

Logic interpretations define the relationships between real-world entities and their logic representations. We introduce an explicit structure for documenting interpretations based on real-world types. As we have demonstrated previously, the benefits of using real-world types can be considerable, but the effort required might deter programmers. In this paper, we introduce a semi-automated mechanism that: (a) synthesizes candidate real-world types, (b) infers real-world type bindings for program variables, and (c) synthesizes candidate type rules from verified or trusted programs. We illustrate the synthesis approach using an open-source project for which we have previously developed a complete real-world type system.

Model-based development of software using tools such as MathWorks Simulink has become common in the engineering of safety-critical systems. When working with Simulink, engineers need to be able to assure that the subject models possess crucial properties such as: (1) safety properties are met, (2) the use of measurement units is consistent, (3) freedom from exceptions, (4) the execution sequences of blocks is as planned, and (5) data types are inferred properly. In this paper, we describe: (a) an approach to the graphic decoration of Simulink models to display information determined by formal verification, and (b) a system, SimulinkDec, that implements the decoration. Block colouring, enhancements to block textual descriptions, and comments are used to present the information of interest to the user. SimulinkDec provides a graphical user interface that allows engineers to easily perform formal verification and display the results of that analysis.

The Zimbabwean medicinal plant Monadenium lugardae was evaluated as a potential source of new anticancer constituents. Four new tetracyclic triterpene (1-4) were isolated, accompanied by four previously known triterpenes (5-8). Against a panel of human tumor cell lines, lugardstatins 1 (1) and 2 (2) had good cancer cell growth inhibitory activity. All of the triterpene structures (1-8) were established by 1D and 2D NMR spectrometric and HR mass spectrometric analysis.

Cyber security research has produced numerous artificial diversity techniques such as address space layout randomization, heap randomization, instruction-set randomization, and instruction location randomization. To be most effective, these techniques must be high entropy and secure from information leakage which, in practice, is often difficult to achieve. Indeed, it has been demonstrated that well-funded, determined adversaries can often circumvent these defenses. To allow use of low-entropy diversity, prevent information leakage, and provide provable security against attacks, previous research proposed using low-entropy but carefully structured artificial diversity to create variants of an application and then run these constructed variants within a fault-tolerant environment that runs each variant in parallel and cross check results to detect and mitigate faults. If the variants are carefully constructed, it is possible to prove that certain classes of attack are not possible. This paper presents an overview and status of a cyber fault tolerant system that uses a low overhead multi-variant execution environment and precise static binary analysis and efficient rewriting technology to produce structured variants which allow automated verification techniques to prove security properties of the system. Preliminary results are presented which demonstrate that the system is capable of detecting unknown faults and mitigating attacks.

Cyber-physical systems model and react to changes in physical phenomena. Modeling introduces the possibility of error, yet physical properties of physical phenomena are poorly represented in common programming and modeling languages. We present an approach to encoding and analyzing dimensions, units, and scale factors. Our approach appends physical properties to SIMULINK block names using an easy-to-read and easy-to-write syntax. For example, a SIMULINK block that outputs a force might be named Force (kg m/s"2) or Force (N). Our approach provides static analysis using PVS: Simulink 2PVS translates SIMULINK models into PVS, and PVS proves consistent use of physical properties during type checking. Our approach enables engineers to detect defects arising from mistakes in handling physical properties during development. Detecting these defects during development both decreases overall system cost and increases overall system dependability.

Software systems sense and affect real world objects and processes in order to realize important real-world systems. For these systems to function correctly, such software should obey constraints inherited from the real world. Typically, neither important characteristics of real-world entities nor the relationships between such entities and their machine-world representations are specified explicitly in code, and important opportunities for detecting errors due to mismatches are lost. To address this problem we introduce real-world types to document in software both relevant characteristics of real-world entities and the relationships between real-world entities and machine-level representations. These constructs support specification and automated static detection of such mismatches in programs written in ordinary languages. We present a prototype implementation of our approach for Java and case studies in which previously unrecognized real-world type errors in several real systems were detected.

The public reporting burden for this collection of information is estimated to average 1 hour per response, including the time for reviewing instructions, searching existing data sources, gathering and maintaining the data needed, and completing and reviewing the collection of information.

In any safety argument, belief in the top-level goal depends upon a variety of assumptions that derive from the system development process, the operating context, and the system itself. If an assumption is false or becomes false at any point during the lifecycle, the rationale for belief in the safety goal might be invalidated and the safety of the associated system compromised. Assurance that assumptions actually hold when they are supposed to is not guaranteed, and so monitoring of assumptions might be required. In this paper, we describe the Safety Condition Monitoring System, a system that permits comprehensive yet flexible monitoring of assumptions throughout the entire lifecycle together with an alert infrastructure that allows tailored responses to violations of assumptions. An emphasis of the paper is the approach used to run-time monitoring of assumptions derived from software where the software cannot be easily changed.

Quantitative methods are usually preferred in safety assessment, but, frequently, necessary probabilities cannot be determined accurately. As a result, expert judgment plays a significant role in safety arguments and system deployment decisions. Trust in expert judgment is based on the assumption that the expert's experience, knowledge, and training will enable the expert to make a suitable decision. The record indicates, however, that this assumption does not always hold and that decisions tend to be ad hoc and unprincipled. In this paper we present an analysis of expert judgment and a rigorous process for utilizing expert judgment in safety arguments.