Writing threat detection signatures directly from informal reports is error-prone and may omit critical details. Attack trees provide a rigorous model for specifying complex threats, but bridging the gap between attack trees and implementable detection logic requires a formal methodology. In this paper, we present a correct-by-construction approach for generating threat detections from attack trees. We formalize the trace semantics of attack trees, defining precisely the sets of event traces corresponding to successful attacks. We also provide a formal semantics for the Generic Threat Detection Language (GTDL), a simplified fragment of a production detection language used in a commercial security product (Bitdefender ( https://www.bitdefender.com )), focusing on detection logic essential for practical deployment. We then give a structural translation from attack trees to GTDL, encoding sequencing, choice, and parallelism directly at the level of event traces. We prove that this translation is sound: every event trace detected by the GTDL signature corresponds to a valid attack trace permitted by the original attack tree semantics, and vice versa. By aligning high-level threat models with executable detection logic in operational security products, our results enable the automated synthesis of provably correct and robust detection signatures for real-world environments.
Formal SMT modeling of programs remains less intuitive than programming, despite shared logical foundations. This paper argues that three high-level features, (1) bounded arbitrary-precision integers, (2) simplified struct syntax, and (3) template metaprogramming, are essential to bridge this gap. Unlike shallow SMT-LIB wrappers or direct SMT-LIB usage, these features enable program-like modeling with automated constraint propagation and compile-time code generation, thereby lowering the learning curve and boosting productivity. We also identify key compiler challenges unique to implementing these features.
The widespread deployment of reinforcement learning (RL) systems in real-world applications necessitates rigorous guarantees of their correctness. In the RL system, an agent iteratively interacts with the environment, with the objective of maximizing cumulative rewards. These interactions involve constraints of states, actions, and rewards, where any violation of these constraints indicates a system-level error. In this paper, we propose an SMT-based framework for the formal modeling of RL systems. Our method encodes constraints for RL components as SMT formulas, and cumulative reward maximization as an optimization objective, enabling automated verification of constraint satisfiability through SMT solvers. We evaluate our formal modeling approach through experiments conducted on a popular RL environment. Experimental results validate the effectiveness of our method in identifying constraint violations and ensuring behavioral correctness.
Neural-Symbolic Systems (NSSs) have been widely deployed in safety-critical domains. However, due to the inherent uncertainty and opaqueness of DNNs, there is an increasing demand for security assurance. In this work, we propose an adjustment framework based on runtime verification (RV, for short) to ensure NSS compliance with given signal temporal logic (STL) properties. To identify unsafe control signal in time, we utilize Runge-Kutta method to predict the system trajectory under scrutiny at discrete time-steps. Our framework also supports the switching of control signals upon violation of safety properties. This capability is achieved through the deployment of predictive strategies, including the construction of a state tree and forward-search algorithms, enabling the system to dynamically select and switch to alternative control signals in real time. We conduct an evaluation on publicly available control systems. The evaluation results show that our method successfully repairs critical safety issues, and significantly improves the reliability of NSSs.
Synthesizing ranking functions is a typical technique for proving loop termination. In this work, we propose an approach to handle the backward, or the reverse, problem. That is, one constructs loops such that a given linear function is a ranking function for these loops. To achieve this, we firstly demonstrate by experiments the necessity to introduce parameters to increase the success ratio. We then formulate this problem as a proper existential quantifier elimination (or parametric system solving) problem, and propose two efficient methods to handle it. We have implemented our methods and demonstrated their effectiveness by extensive experiments.
