Arya (TA3)

For DARPA HACCS Technical Area 3, we developed implantable software agents, Arya Agents, that seek and destroy bot implants in target networks.  These agents can traverse unknown and diverse networks and perform complex bot neutralization actions without centralized control, providing unprecedented levels of safety and reliability.  The deployed agents are highly-efficient in terms of space and compute, demonstrated to function on severely resource-constrained IoT devices.  The agent includes advanced, portable, and autonomous capabilities for exploitation, staging, lateral movement, reasoning about complex network and subnetwork topology, host intelligence gathering, passive capture, active scanning, device and service identification, network traffic redirection, routing modifications, and host resource actions (e.g., files, networks, accounts, and permissions).  

The Arya agent has been demonstrated safe, efficient, and effective in multiple fully autonomous HACCS evaluation operations on diverse real-world networks. It is fully functional on resource-constrained IoT devices such as routers, IP cameras, and smart plugs. The agent has multiple least-common-denominator static builds (e.g., Linux ARMv5, Linux MIPS-I, Linux i386, and Windows Win32) and no software dependencies on the target system.

We developed a rigorous and structured ontology that describes the entities with which the agent can sense and interact.  Agents reason about the state of the operation and their tactical choices via the entity ontology. For the HACCS program, we have prototyped a domain-specific language, the Arya Language, that enables developers to create customizable agents as required by a particular operation.  The Arya Language enables the specification of agent tactics and techniques.  Techniques can be combined into tactics using condition variables and preconditions on actions.  The language exposes the agent state via the entity language and enables the complexities of a target network to be abstracted.

The rules of engagement of a particular operation guide Arya Agent actions.  The RoE are specified in a language that specifies permissions on actions (from the action language) as applied to entities in the operational language.  The RoE language is rigorously specified in the Coq formal proof system, and a policy checker has been implemented in Coq.  We have extracted the policy checker to C++, and each agent carries this verified implementation to check actions against policy before an action is initiated.

The Arya agent includes state-of-the-art mechanisms for autonomous and decentralized operations.  For HACCS, our team has developed a bespoke, embedded shared ledger that pioneered proof-of-burn as a low-cost consensus mechanism.  Shared state updates are rare, and the traffic produced by the shared ledger is configurable, with updates communicated over our optimized overlay network.  We have also developed a novel ledger partition resolution algorithm that enables disconnected agent operation with possible eventual reconnection.  Agents can operate in partially denied environments without centralized control.  In addition, the ledger provides a distributed audit trail for operations.

The Arya agent includes an overlay network that abstracts away the complexities of diverse network topologies and supports both efficient broadcast and optimally-routed (with respect to the overlay) peer-to-peer communication across networks.  The overlay supports configurable, probabilistically redundant connections, encryption, and authentication.  We have pioneered an addressing mechanism with a short identifier that encodes the routing information necessary to route a message from one agent to another at interface granularity, through NATs.  Furthermore, the overlay is a modularized component that can be swapped out at configuration time for a mechanism that more closely matches the threat under emulation.