A device to prevent, detect and respond to one or more security threats between one or more controlled hosts and one or more services accessible from the controlled host. The device determines the authenticity of a user of a controlled host and activates user specific configurations under which the device monitors and controls all communications between the user, the controlled host and the services. As such, the device ensures the flow of only legitimate and authorized communications. Suspicious communications, such as those with malicious intent, malformed packets, among others, are stopped, reported for analysis and action. Additionally, upon detecting suspicious communication, the device modifies the activated user specific configurations under which the device monitors and controls the communications between the user, the controlled host and the services.

The Unified Cross Domain Management Office (UCDMO) states that its mission is to provide coordination and oversight for the cross domain community’s vision of “secur[ing] cross domain access to and sharing of timely and trusted information, creating a seamless Enterprise that enables decision advantage.” The UCDMO defines three types of cross domain solution (CDS) — transfer, access and multi-level — to satisfy this vision.
The transfer CDS, or guard, moves information securely between software applications running in different information security domains. Since the guard must approve all information flows between domains, it is traditionally deployed on a standalone computer host that provides the only physical link between the domains’ networks. This deployment strategy ensures that the guard cannot be bypassed. Unfortunately, as the demand for sharing increases, this strategy can prove costly.  Data centers, for example, may charge more for custom guard hardware that cannot be reallocated easily for other uses

A graph G with q edges is said to be harmonious if there is an injection f  from the vertices of G to the group of integers modulo q such that when each edge xy is assigned the label f (x) + f (y) (mod q), the resulting edge labels are distinct. If G is a tree, exactly one label may be used on two vertices. Over the years, many variations of harmonious labelings have been introduced.
We study a variant of harmonious labeling. A function f  is said to be a properly even harmonious labeling of a graph G with q edges if f  is an injection from the vertices of G to the integers from 0 to 2 (q-1) and the induced function f*  from the edges of G to 0,2,…,2 (q-1) defined by f* (xy) = f (x) + f (y) (mod 2q) is bijective. We investigate the existence of properly even harmonious labelings of families of disconnected graphs with one of C3, C4, K4 or W4as a component.

Architecture description languages such as AADL allow systems engineers to specify the structure of system architectures and perform several analyses over them, including schedulability, resource analysis, and information flow. In addition, they permit system-level requirements to be specified and analyzed early in the development process of airborne and ground-based systems. These tools can also be used to perform safety analysis based on the system architecture and initial functional decomposition. Using AADL-based system architecture modeling and analysis tools as an exemplar, we extend existing analysis methods to support system safety objectives of ARP4754A and ARP4761. This includes extensions to existing modeling languages to better describe failure conditions, interactions, and mitigations, and improvements to compositional reasoning approaches focused on the specific needs of system safety analysis. We develop example systems based on the Wheel Braking System in SAE AIR6110 to evaluate the effectiveness and practicality of our approach.

A graph G with q edges is said to be harmonious if there is an injection f  from the vertices of G to the group of integers modulo q such that when each edge xy is assigned the label f (x) + f (y) (mod q), the resulting edge labels are distinct. If G is a tree, exactly one label may be used on two vertices. Over the years, many variations of harmonious labelings have been introduced.
We study a variant of harmonious labeling. A function f  is said to be a properly even harmonious labeling of a graph G with q edges if f is an injection from the vertices of G to the integers from 0 to 2 (q-1) and the induced function f*  from the edges of G to 0 to 0,2,…,2 (q-1) defined by f* (xy) = f (x) + f (y) (mod2q) is bijective. This paper focuses on the existence of properly even harmonious labelings of the disjoint union of cycles and stars, unions of cycles with paths, unions of squares of paths, and unions of paths.

This annex is intended to help component vendors and system integrators using the (Future Airborne Capability Environment) FACE Technical Standard. FACE Technical Standard Edition 3.0 provides a data modeling architecture but does not provide mechanisms for describing component behavior or timing properties. This document provides guidance for translating a FACE Standard Edition 3.0 Data Architecture XMI model into AADL so that behavior and timing properties can be added and analyzed.

This annex supports the modeling, analysis, and integration of FACE artifacts in AADL. It gives AADL style guidelines and an AADL property set to provide a common approach to using AADL to express architectures that include FACE components. Using common properties and component representations in AADL makes AADL models of FACE components portable and reusable and increases the utility of tools that operate on such AADL models.

Model-based development tools are increasingly being used for system-level development of safety-critical systems. Architectural and behavioral models provide important information that can be leveraged to improve the system safety analysis process. Model-based design artifacts produced in early stage development activities can be used to perform system safety analysis, reducing costs, and providing accurate results throughout the system life-cycle. In this paper we describe an extension to the Architecture Analysis and Design Language(AADL) that supports modeling of system behavior under failure conditions. This Safety Annex enables the independent modeling of component failures and allows safety engineers to weave various types of fault behavior into the nominal system model. The accompanying tool support uses model checking to propagate errors from their source to their effect on top-level safety properties without the need to add separate propagation specifications. Our tools are also able to compute minimal cutsets for these errors to produce faults trees familiar to safety engineers and certification authorities. We describe the Safety Annex, illustrate its use with a representative example, and discuss and demonstrate the tool support enabling an analyst to investigate the system behavior under failure conditions.

Challenging problems associated with system software complexity growth are threatening industry’s ability to build next generation safety- and security-critical embedded cyber physical weapon systems including vertical lift avionics systems. Contributors to these problems include the growth of software enabled capabilities, interaction complexity in system integration, and ambiguous, missing, incomplete, and inconsistent requirements. Problems continue to hamper systems in the areas of resource utilization, timing and scheduling, concurrency and distribution, and safety and security. A new approach called Architecture Centric Virtual Integration Process (ACVIP), based on the SAE International® Aerospace Standard AS5506C Architecture Analysis and Design Language (AADL), is being developed and investigated by the United States (US) Army to address these challenges. ACVIP is a compositional, quantitative, architecture-centric, model-based approach enabling virtual integration analysis in the early phases and throughout the lifecycle to detect and remove defects that currently are not found until software, hardware, and systems integration and acceptance testing. The Science & Technology (S&T) program called Joint Multi-Role (JMR) Technology Demonstrator (TD) with the Mission System Architecture Demonstration effort is developing, piloting, evaluating and maturing Modular Open Systems Approach (MOSA), a Comprehensive Architecture Strategy (CAS), and Model Based Engineering (MBE) including ACVIP through a number of projects with contractor teams to prepare for the Future Vertical Lift (FVL) family-of-systems. ACVIP plays a key role in addressing issues in cyber-physical systems (CPS) and can be a key contributor to the US Department of Defense (DoD) Digital Engineering Strategy. It provides a well-defined standard as a foundation for a commercial tool marketplace, a ready base for ongoing efforts in maturation and commercialization of the technology, provides early demonstrations of success, and a unique architectural contribution to authoritative source of truth (ASoT). We will first discuss the challenges in CPS development and the contribution ACVIP makes to address these challenges. We then outline how ACVIP is a key component that contributes to all five goals of the DoD Digital Engineering Strategy.

PKCS#11, also known as Cryptoki, is a widely adopted C-language API and interoperability standard for communicating with cryptographic libraries. While comprehensive and prescriptive, the standard is also extremely complex. The base specification alone describes approximately 50 functions through over 100 pages of documentation. Add-on specifications provide additional functionality, but also impose additional complexity. As the standard evolves through collaboration and expansion, new areas of imprecision and ambiguity are introduced which make it difficult for vendors to implement libraries that are 100% functionally accurate and compliant with the specification. Users of cryptographic libraries are familiar with the industry reality that PKCS#11 libraries will not always interoperate flawlessly with each other. In the best case, these divergences result in development delays as build issues and functional deficiencies are root-caused and remedied. In the worst case, customers may face production outages or data corruption due to incorrect assumptions or imperfect testing.

To address this problem at its core, Galois has developed an API specification and testing framework that captures the complex behaviors of Cryptoki in a mathematical specification language. This specification, in turn, is used to automatically synthesize a test suite that enforces compliance with (a mathematical model of) the PKCS#11 standard. The approach, known as model-based testing, was used to generate a corpus of PKCS#11 compliance tests that provide complete test coverage over the formal model.

While model-generated tests are designed to enforce compliance with the PKCS#11 standard, they have also proven effective at keeping bugs out of production. Error handling scenarios defined in the standard often represent corner cases which, if not properly handled by implementation code, will cause program crashes or other serious defects. Because the aim of model-based testing is to generate test cases for all the behaviors in the standard, errors of this variety are naturally uncovered with compliance tests. As a result, assuring PKCS#11 libraries with model-generated compliance tests leads to client applications that are portable, more robust and have fewer security vulnerabilities.

Over the past 20 years, a variety of automated software diversity techniques have been proposed. Some techniques randomize aspects of the implementation that are left undefined by the source language specification, such as code layout, stack layout, or locations of heap-allocated objects. Others insert instrumentation or obfuscation that is transparent from an application perspective, e.g. using XOR masks to obscure data values in memory or hiding code pointers using jump tables. A common assumption is that layering these techniques improves security due to increased entropy in the resulting binary. In this paper we examine this assumption and show that it fails to hold in general. In particular, it fails in one of the strongest deployment models for software diversity—that of multiple diverse variants running together in a multi-variant execution environment (MVEE) where attacks manifest as detectable behavioral divergence. We present several examples of diversity combinations that are vulnerable to attack in an MVEE even when none of the component techniques are vulnerable in isolation. Based on these results, we present guidance on which techniques do combine well and suggestions for effective deployment of diversity in MVEEs.

Presented at the Layered Assurance Workshop (LAW), 2016
https://www.acsac.org/2016/workshops/law