Logic rules allow analysis of complex relationships to be expressed easily, especially for transitive relations in critical applications. However, understanding and predicting the efficiency of different inference methods remain challenging, even for simplest rules given different kinds of input data. This paper analyzes the efficiency of all three types of well-known inference methods – query-driven, ground-and-solve, and fact-driven – along with their respective optimizations, and compares with optimal complexities for the first time, for analyzing transitive graph relations. We also experiment with rule systems widely considered to have the best performance. We analyze all well-known rule variants and widely varying input graphs. The results include precisely calculated optimal time complexities; comparative analysis across different inference methods, rule variants, and graph types; confirmation with performance experiments; as well as discovery of a performance bug.

Robust access control is a cornerstone of secure software, systems, and networks. An access control mechanism is as effective as the policy it enforces. However, authoring effective policies that satisfy desired properties such as the principle of least privilege is a challenging task even for experienced administrators. In this paper, we set out to address this pain point by proposing Restricter, which automatically tightens each (permit) policy rule of a policy with respect to an access log, which captures some already exercised access requests and their corresponding access decisions (i.e., allow or deny). Restricter achieves policy tightening by reducing the number of access requests permitted by a policy rule without sacrificing the functionality of the underlying system it is regulating. We implement Restricter for Amazon’s Cedar policy language and demonstrate its effectiveness through two realistic case studies.

Advanced Persistent Threat (APT) attacks are sophisticated cyberattacks characterized by stealth, persistence, and long-term engagement with targeted systems. Traditional detection approaches using machine learning and deep learning rely on internal model representations or post hoc explainability techniques, which often lack human-readable context and require significant manual interpretation. This paper investigates the use of large language models (LLMs) for APT detection through code analysis. We evaluate LLMs’ ability to identify APT-related behaviors in code-snippet sequences, localize malicious components, and map them to corresponding MITRE ATT CK tactics, techniques, and procedures (TTPs). To address context-window limitations, we introduce a segmentation-based approach that divides long code sequences into smaller segments and iteratively processes them while preserving context through summary propagation. Because real-world APT data are scarce due to their stealthy nature, privacy constraints, and long attack lifecycles, we construct an APT dataset derived from Caldera adversary profiles and emulation plans. Experimental results show that LLMs, when guided by rubric-based prompts and supplemented with ATT CK domain knowledge, achieve robust performance across detection, localization, and TTP mapping tasks.

Signal Temporal Logic (STL) is a widely adopted specification language for Cyber-Physical Systems that can be used to express critical temporal requirements, such as system safety and response time. STL’s expressivity, however, is not sufficient to capture the cumulative duration during which a property holds within an interval of time. To overcome this limitation, we introduce Cumulative-Time Signal Temporal Logic (CT-STL) which operates over discrete-time signals and extends STL with a new cumulative-time operator. This operator compares the sum of all timesteps for which its nested formula is true with a threshold. We present both a qualitative and a quantitative (robustness) semantics for CT-STL and prove the soundness and completeness of the robustness semantics. We also provide an efficient online monitoring algorithm for both semantics. We demonstrate the utility of CT-STL via two case studies: specifying and monitoring cumulative temporal requirements for a microgrid and an artificial pancreas.

This paper presents Barrier-based Simplex (Bb-Simplex), a new, provably correct design for runtime assurance of continuous dynamic systems. Bb-Simplex is centered around the Simplex control architecture, which consists of a high-performance advanced controller that is not guaranteed to maintain safety of the plant, a verified-safe baseline controller, and a decision module that switches control of the plant between the two controllers to ensure safety without sacrificing performance. In Bb-Simplex, Barrier certificates are used to prove that the baseline controller ensures safety. Furthermore, Bb-Simplex features a new automated method for deriving, from the barrier certificate, the conditions for switching between the controllers. Our method is based on the Taylor expansion of the barrier certificate and yields computationally inexpensive switching conditions. We also propose extensions to Bb-Simplex to enable its use in hybrid systems, which have multiple modes each with its own dynamics, and to support its use when only approximate dynamics (not exact dynamics) are available, for both continuous and hybrid dynamic systems. We consider significant applications of Bb-Simplex to microgrids featuring advanced controllers in the form of neural networks trained using reinforcement learning. These microgrids are modeled in RTDS, an industry-standard high-fidelity, real-time power systems simulator. Our results demonstrate that Bb-Simplex can automatically derive switching conditions for complex continuous and hybrid dynamic systems, the switching conditions are not overly conservative, and Bb-Simplex ensures safety even in the presence of adversarial attacks on the neural controller when only approximate dynamics (with an error bound) are available. Our experiments to evaluate conservativeness of the switching conditions show that switches from an unsafe advanced controller to a baseline controller occur on average only a few control periods before a safety violation would have occurred.

Advanced malware attacks often employ sophisticated tactics such as DLL injection, script-based attacks, and the exploitation of zero-day vulnerabilities. As evidenced by the recent high-profile cyberattacks, these techniques have enabled attackers to infiltrate computer systems that were thought to be well-protected. There is thus an urgent need to enhance current malware defenses with advanced Artificial Intelligence (AI) techniques that can effectively detect in real-time the elusive traces of malware attacks concealed within the extensive realm of normal activities. This paper introduces Graphite, a graph-based approach for real-time detection of advanced malware attacks based on the event data collected from Event Tracing for Windows (ETW). Graphite first abstracts various entities and their relationships embodied within system events into computation graphs, which are amenable to graph-based machine learning methods. As a computation graph can be gigantic, making real-time malware detection inefficient, we project the graph into smaller graphlets, which are then subsequently fed into our graph-based approach to detect malicious activities. Our experimental results show that Graphite achieves 87.7% classification accuracy in offline testing and 86.7% accuracy in real-time detection.

This paper presents a powerful automated framework for making complex systems resilient under failures, by optimized adaptive distribution and replication of interdependent software components across heterogeneous hardware components with widely varying capabilities. A configuration specifies how software is distributed and replicated: which software components to run on each computer, which software components to replicate, which replication protocols to use, etc. We present an algorithm that, given a system model and resilience requirements, (1) determines initial configurations of the system that are resilient, and (2) generates a reconfiguration policy that determines reconfiguration actions to execute in response to failures and recoveries. This model-finding algorithm is based on state-space exploration and incorporates powerful optimizations, including a quotient reduction based on a novel equivalence relation between states. We present experimental results from successfully applying a prototype implementation of our framework to a model of an autonomous driving system.

This tutorial examines well-known algorithms for distributed consensus problems, from classical consensus to blockchain consensus. We discuss exact algorithms that are high-level as in pseudocode and directly executable as programs at the same time, focusing on how to quickly program, configure, run, and check these algorithms as well as distributed algorithms and systems in general.

This chapter introduces AI-Grid: Artificial Intelligence (AI) enabled, provably resilient networked microgrids. We present a programmable platform that integrates reliable AI modeling under uncertainty, reachability analysis, formal control, high-assurance software architectures, and cybersecurity technologies to enable scalable, autonomic, and ultra-resilient microgrids and networked microgrids. This platform has been developed in collaboration with the power industry and the defense sector and is being demonstrated in real-world microgrids.

Modern cyber-physical systems (CPS) interact with the physical world, hence their correctness is important. In this work, we build upon the Simplex Architecture, where control authority may switch from an unverified and potentially unsafe advanced controller to a verified-safe baseline controller in order to maintain system safety. We take the approach further by lifting the requirement that the baseline controller must be verified or even correct, instead also treating it as a black-box component. This change is important; there are many types of powerful control techniques---model predictive control and neural network controllers---that often work well in practice, but are unlikely to be formally proven correct due to complexity. We prove such an architecture maintains safety, and present case studies where model-predictive control provides safety for multi-robot coordination, and unverified neural networks provably prevent collisions for groups of F-16 aircraft.

We present distributed distance-based control (DDC), a novel approach for controlling a multi-agent system, such that it achieves a desired formation, in a resource-constrained setting. Our controller is fully distributed and only requires local state-estimation and scalar measurements of inter-agent distances. It does not require an external localization system or inter-agent exchange of state information. Our approach uses spatial-predictive control (SPC), to optimize a cost function given strictly in terms of inter-agent distances and the distance to the target location. In DDC, each agent continuously learns and updates a very abstract model of the actual system, in the form of a dictionary of three independent key-value pairs (delta s, delta d), where delta d is the partial derivative of the distance measurements along a spatial direction delta s. This is sufficient for an agent to choose the best next action. We validate our approach by using DDC to control a collection of Crazyflie drones to achieve formation flight and reach a target while maintaining flock formation.

This chapter presents a formal method for quantifying the in situ resilience of a microgrid under disturbances. The key innovation is a Signal Temporal Logic-based approach to monitoring the microgrid state against operational specifications. The method does not require knowledge of the system topology and uses locally available data for in situ resilience quantification under varying operating conditions. Case studies verify the applicability of the in situ resilience analysis approach in real time and its superiority over existing methods.

This paper presents a language, Alda, that supports all of logic rules, sets, functions, updates, and objects as seamlessly integrated built-ins. The key idea is to support predicates in rules as set-valued variables that can be used and updated in any scope, and support queries using rules as either explicit or implicit automatic calls to an inference function. We have defined a formal semantics of the language, implemented a prototype compiler that builds on an object-oriented language that supports concurrent and distributed programming and on an efficient logic rule system, and successfully used the language and implementation on benchmarks and problems from a wide variety of application domains. We describe the compilation method and results of experimental evaluation.

Integrating logic rules with other language features is increasingly sought after for advanced applications that require knowledge-base capabilities. To address this demand, increasingly more languages and extensions for such integration have been developed. How to evaluate such languages? This paper describes a set of programming and performance benchmarks for evaluating languages supporting integrated use of rules and other features, and the results of evaluating such an integrated language together with logic languages and languages not supporting logic rules.

We introduce Spatial Predictive Control (SPC), a technique for solving the following problem: given a collection of robotic agents with black-box positional low-level controllers (PLLCs) and a mission-specific distributed cost function, how can a distributed controller achieve and maintain cost-function minimization without a plant model and only positional observations of the environment? Our fully distributed SPC controller is based strictly on the position of the agent itself and on those of its neighboring agents. This information is used in every time step to compute the gradient of the cost function and to perform a spatial look-ahead to predict the best next target position for the PLLC. Using a simulation environment, we show that SPC outperforms Potential Field Controllers, a related class of controllers, on the drone flocking problem. We also show that SPC works on real hardware, and is therefore able to cope with the potential sim-to-real transfer gap. We demonstrate its performance using as many as 16 Crazyflie 2.1 drones in a number of scenarios, including obstacle avoidance.

As machine learning models find broader applications in cybersecurity, the importance of model explainability becomes more evident. In the area of malware detection, where the consequence of misclassification can be severe, explainability becomes crucial. AI explainers not only help understand the reasons behind malware classifications but also assist in finetuning models to improve detection accuracy. Additionally, AI explainers can serve as a valuable tool for error detection, ensuring accountability, and mitigating potential biases. In this paper, we demonstrate how AI explainers can play a vital role in identifying issues in data collection and enhancing our comprehension of the model's classification results. Our analysis of explanation results reveals several issues within the data collection process, including event loss and the presence of environment-specific information. Additionally, we have identified mislabelled samples based on the explanation results and shared lessons learned from our data collection efforts.

Spreadsheets are enormously popular because they enable non-programmers to create applications that manipulate tabular data. The core functionality of many web applications is to display and manipulate tabular data, typically stored in databases. These observations inspired the design of WebSheets, a no-code/low-code web application development framework that provides novel support for security and privacy. The key innovation of WebSheets is that fine-grained, data-driven security policies, as well as application logic, are expressed in the spreadsheet paradigm. This empowers data owners, who are often non-programmers, to directly implement their desired security policies. Each data table in WebSheets is paired with a permission table, which is editable only by the data table's owner. Formulas in a permission table define who can read and write cells in the associated data table. These formulas can easily express role-based, attribute-based and relationship-based access control policies as well as delegation. WebSheets guarantees that these policies are enforced during the entire lifetime of every data item, as it flows through calculations within an application and even when it is passed between applications. While providing global privacy guarantees similar to information flow control systems, WebSheets enables end users to work with the more familiar access control policies. Any user wishing to safeguard their data should store them in tables they own, thereby requiring all web applications to access their data by referencing their tables. This ensures that all applications will respect their access policies in the associated permission tables. By automatically filtering out inaccessible rows and columns, WebSheets presents user-customized views that are the key feature of many web applications. Additional key features of WebSheets include: secure and scalable distributed evaluation techniques that confine WebSheets computations using OS-based access control and sandboxing mechanisms to enforce the principle of least privilege; secure integration with external systems, including web servers, databases, web browsers, user interfaces, and external modules. The benefits of distributed, least-privilege evaluation extend to modules written in any language; policy analysis, including novel techniques to help users understand policies and debug policy errors, and to improve policies over time, either to correct problems or respond to changes in use; and expressive formula language that features first-class tables, seamless integration of access control and input validation, and support for declassification. Web application vulnerabilities have been the dominant cause of data breaches in recent years. As defenses against lower-level vulnerabilities have come to be widely deployed, attackers are targeting higher-level errors. WebSheets addresses the following three common types of higher-level errors. Omitted or incorrectly coded security policies. Key stakeholders in data privacy are typically non-programmers that need to first communicate their security requirements to developers that then implement them. Developers may misunderstand the desired policies or implement simpler, relaxed policies as a result of pressure to deliver required functionality on time. In WebSheets, data owners can directly express desired fine-grained security policies using formulas. Incorrect placement of security checks. Today, policies are enforced mainly by ad-hoc placement of security checks throughout a web application's code. This lack of separation of concerns makes it hard to check whether important security policies are correctly implemented and soundly enforced by complete mediation. In WebSheets, security policies are separated from other application logic and enforced automatically on all data paths. Vulnerabilities that create unintended dataflows. Command and data injection vulnerabilities provide avenues for attackers to create new data flows, allowing data breaches to occur. The underlying problem is that web applications generally execute with a superset of the privileges available to all end users. In contrast, WebSheets by default executes with the privilege of the requesting user. Hence, data inaccessible to that user won't be leaked or corrupted, despite vulnerabilities in the application code or the WebSheets evaluation engine. WebSheets is related to commercial no-code and low-code web application development frameworks for creating mobile apps and web apps centered around interacting with tabular data stored in databases or spreadsheets, such as Google AppSheet and Glide Apps, but they lack WebSheets's key features listed above. This is joint work with R. Sekar. Preliminary work on WebSheets is described in [1,2].

The Simplex Architecture is a runtime assurance framework where control authority may switch from an unverified and potentially unsafe advanced controller to a backup baseline controller in order to maintain the safety of an autonomous cyber-physical system. In this work, we show that runtime checks can replace the requirement to statically verify safety of the baseline controller. This is important as there are many powerful control techniques, such as model-predictive control and neural network controllers, that work well in practice but are difficult to statically verify. Since the method does not use internal information about the advanced or baseline controller, we call the approach the Black-Box Simplex Architecture. We prove the architecture is safe and present two case studies where (i) model-predictive control provides safe multi-robot coordination, and (ii) neural networks provably prevent collisions in groups of F-16 aircraft, despite the controllers occasionally outputting unsafe commands.