Inigo Incer

We propose a conceptual approach to securing cyber-physical systems (CPS): the Cyber-Physical Immune System (CPIS), a collection of hardware and software elements deployed on top of a conventional CPS. Inspired by its biological counterpart, the CPIS comprises an independent network of distributed computing units that collects data from the conventional CPS, utilizes data-driven techniques to identify threats, adapts to the changing environment, alerts the user of any threats or anomalies, and deploys threat-mitigation strategies.

Assume-guarantee (AG) are formal specifications for components in a system that make explicit what the component assumes from its environment and what is required from the component being specified when the environment meets the assumptions of the contract. In AG contracts, the assumptions and guarantees are expressed using trace properties. Some security and robustness properties cannot be expressed using trace properties and need hyperproperties for their representation. Hypercontracts extend AG contracts by allowing arbitrary structured hyperproperties to be used to define the assumptions and guarantees of the specification. This papers introduces the algebra of hypercontracts.

Seeking the largest solution to an expression of the form Ax ≤ B is a common task in several domains of engineering and computer science. This largest solution is commonly called quotient. We introduce an algebraic structure called preorder heap (preheap) which enables the closed-form expression of quotients. If solving Ax ≤ B is relevant to your application, check whether your theory is a preheap; if so, you immediately have a quotient.

Proofs for claims made in 'Coherent Extension, Composition, and Merging Operators in Contract Models for System Design.'

Contract models have been proposed to promote and facilitate reuse and distributed development. In this paper, we cast contract models into a coherent formalism used to derive general results about the properties of their operators. We study several extensions of the basic model, including the distinction between weak and strong assumptions and maximality of the specification. We then analyze the disjunction and conjunction operators, and show how they can be broken up into a sequence of simpler operations. This leads to the definition of a new contract viewpoint merging operator, which better captures the design intent in contrast to the more traditional conjunction. The adjoint operation, which we call separation, can be used to re-partition the specification into different viewpoints. We show the symmetries of these operations with respect to composition and quotient.

This paper describes a component-based concurrent model of computation for reactive systems. The components in this model, featuring ports and hierarchy, are called reactors. The model leverages a semantic notion of time, an event scheduler, and a synchronous-reactive style of communication to achieve determinism. Reactors enable a programming model that ensures determinism, unless explicitly abandoned by the programmer. We show how the coordination of reactors can safely and transparently exploit parallelism, both in shared-memory and distributed systems.

We propose a measure and a metric on the sets of infinite traces generated by a set of atomic propositions. To compute these quantities, we first map properties to subsets of the real numbers and then take the Lebesgue measure of the resulting sets. We analyze how this measure is computed for Linear Temporal Logic (LTL) formulas. An implementation for computing the measure of bounded LTL properties is provided and explained. This implementation leverages SAT model counting and effects independence checks on subexpressions to compute the measure and metric compositionally.

The algebra of assume-guarantee (AG) contracts was introduced to provide technical counterparts to the legal commitments between parties in a supply chain. It was not known whether the AG algebra had a notion of quotient, i.e., the adjoint of composition. This paper settles that question in the affirmative, and provides a closed-form expression for the quotient.

We propose monotonic classification with selection of monotonic features as a defense against evasion attacks on classifiers for malware detection. The monotonicity property of our classifier ensures that an adversary will not be able to evade the classifier by adding more features. We train and test our classifier on over one million executables collected from VirusTotal.
Microsoft implemented our proposed mechanism in its Defender ATP, and the technique was key in stopping the LockerGoga ransomware. The coverage links provide more information.