Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in trustworthy systems, e.g., cryptographic routines. We present a theory of forward symbolic execution for unstructured programs suitable for use in theorem provers that enables automated verification of both functional and non-functional program properties. The theory’s foundation is a set of inference rules where each member corresponds to an operation in a symbolic execution engine. The rules are designed to give control over the tradeoff between the preservation of precision and introduction of overapproximation. We instantiate our theory for BIR, a previously proposed intermediate language for binary analysis. We demonstrate how symbolic executors can be constructed for BIR with common optimizations such as pruning of infeasible symbolic states. We implemented our theory in the HOL4 theorem prover using the HolBA binary analysis library, obtaining machine-checked proofs of soundness of symbolic execution for BIR. We practically evaluated two applications of our theory: verification of functional properties of RISC-V binaries and verification of execution time bounds of programs running on the ARM Cortex-M0 processor. The evaluation shows that such verification can be automated with moderate overhead on medium-sized programs.

Cyber attacks are getting smarter every year, yet most security checks still happen late in the project, when fixes are hardest and costliest. To change that, we propose FreeCAT, a step-by-step “security copilot” that works from the first design sketch all the way to day-to-day operation. FreeCAT automatically turns models, documentation, and log files into easy-to-read threat maps that show which parts of a system hackers would target first. It then runs simulations to test different defenses, points human testers to the riskiest spots, and feeds every new finding back into the map so the picture stays up to date. An AI component speeds up chores such as writing audit reports or checking compliance rules. Because these activities repeat in short loops throughout development and after launch, organizations can spot weak points early, use security budgets where they matter most, and keep pace with new attack tactics without hiring an army of specialists. The current paper outlines the concept and planned building blocks; the full platform will be assembled and validated in future work.

Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic GA, which interprets postconditions relative to program points when these are first encountered. The logic supports both partial and total correctness, derives contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of GA have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, which supports the ARMv6, ARMv8 and RISC-V instruction sets.

Concealing distinguishing features in traffic patterns used in Traffic Analysis (TA) attacks also affects network observability and hence it is detrimental for legitimate traffic analysis (e.g., network monitoring, anomaly detection). The problem is particularly relevant in microservice-based cloud-native systems. In this paper we introduce a novel method that defends traffic flows against TA attacks and selectively exposes metadata to allow semi-trusted entities to recover certain traffic characteristics with low additional overhead by using a surplus area in the packets. In our architecture, proxies protect traffic between microservices using application-level logic and protocol features. We provide a PoC implementation and evaluation of the proposed method using the QUIC and HTTP/3 protocols for two network functions in the 5G Core Network and in a microservice benchmark application. We show that two events can be made indistinguishable for a storage channel attacker, while maintaining observability for a legitimate TA node. We also extend our defense to reduce the accuracy of a more powerful (timing channel) attacker by 20–30%.

Complex coordination protocols are necessary to manage complex organisations. The healthcare management sector is no exception, since different authorities, users, and systems have to interact with each other in order to achieve their organisational goals. In this paper we consider a case study on the authorisation and accreditation of healthcare structures in the Emilia Romagna region in Italy. We specify the case study using global choreographies so to enable the analysis of the correctness of its communication patterns using the Chemical structure diagram showing a molecule with a central carbon atom bonded to a bromine atom, a methyl group, and a hydroxyl group. The structure is labeled with the text "BrmChO" in blue. tool. This requires to refine A flow chart with a central node labeled "PomCho." The chart appears to have a minimal design with no visible connections or additional nodes. The background is plain white. and its underlying theoretical framework. First, we extend Flow chart depicting a process with a central node labeled "PomCho." The chart likely illustrates steps or decisions related to this central concept, with potential branches or connections not visible in the image. to support not only asynchronous communication, but also synchronous one. Moreover, in both the cases, we provide a more efficient algorithm to check closure properties ensuring realisability of choreographies. The new algorithm allows us to check realisability of larger pomsets than before, which makes our approach viable for complex systems such as our case study.

Modern safety-critical and real-time systems increasingly rely on multi-core architectures, which introduce shared hardware resources that can lead to inter-core interference. This interference poses risks to both security and safety, enabling timing side channels and Denial of Service (DoS) attacks. This paper presents a methodology for evaluating the memory hierarchy of hardware platforms, focusing on timing interference and side-channel leakage. Using the OpenPiton platform, we identify and characterize a cross-core covert channel and demonstrate a proof-of-concept side-channel attack exploiting the Network-on-Chip (NoC). Additionally, we evaluate the impact of NoC contention on the worst-case execution time (WCET) of safety-critical applications. Despite exploring software-based mitigations, we find that covert channels cannot be completely eliminated without significant performance trade-offs.

Modern microservice architectures pose challenges in understanding and managing the complex workflows within these decentralized services. In particular, it is difficult to identify anomalous behavior that could indicate a bug or attack. We use traces of microservice application activity (requests and responses) to infer a model of the application’s normal behavior. Our approach mines Petri nets to formally represent concurrent operations and their temporal dependencies with a targeted delay injection approach that accurately and efficiently learns these dependencies. The models produced are both explainable and easy to inspect, which offers more transparency and control. Our evaluation shows that injecting delays during model training allows us to achieve perfect model and log fitness (Move-Model and Move-Log fitness of 1) with just 29 traces. In contrast, a straightforward approach requires over 10,000 traces to achieve similar accuracy. Our models successfully identify anomalies in various experiments, such as traces with one missing or multiple missing activities, and reordered sequences to simulate issues in real-world scenarios. Our approach outperforms the state-of-the-art method, demonstrating higher accuracy.

Partitioning kernels often face challenges such as static resource allocation and insufficient temporal protection, limiting their applicability in dynamic and mixed-criticality systems where resource needs and security boundaries evolve over time. To address these limitations, we present S3K, a capability-based multicore partitioning kernel for embedded RISC-V systems. S3K provides robust spatial and temporal isolation, time protection, and dynamic resource reconfiguration, enabling flexible adaptation to changing operational requirements while maintaining strong safety and security guarantees. Its capability-based model ensures secure and efficient resource management, while in-kernel data partitioning prevents information leakage and mitigates side-channel attacks. Additionally, S3K's scheduler guarantees deterministic process dispatch, free from microarchitectural interference. Evaluation results demonstrate S3K's effectiveness, showing the absence of scheduling jitter, resistance to intra-core side-channels, and efficient inter-process communication. These results highlight S3K's suitability for safety-critical and security-critical applications in dynamic, resource-constrained environments.

We introduce a proof-producing symbolic execution tool for formal verification of P4 programs. The tool has been implemented using the interactive theorem prover HOL4 and results are proved sound with respect to the HOL4P4 formalisation of the P4 language. Most notably, this is a general tool for proving functional correctness that can be applied to entire real-world P4 programs.

Software-Defined Networking (SDN) has transformed network architectures by decoupling the control and data-planes, enabling fine-grained control over packet processing and forwarding. P4, a language designed for programming data-plane devices, allows developers to define custom packet processing behaviors directly on programmable network devices. This provides greater control over packet forwarding, inspection, and modification. However, the increased flexibility provided by P4 also brings significant security challenges, particularly in managing sensitive data and preventing information leakage within the data-plane. This paper presents a novel security type system for analyzing information flow in P4 programs that combines security types with interval analysis. The proposed type system allows the specification of security policies in terms of input and output packet bit fields rather than program variables. We formalize this type system and prove it sound, guaranteeing that well-typed programs satisfy noninterference. Our prototype implementation, TAP4S, is evaluated on several use cases, demonstrating its effectiveness in detecting security violations and information leakages.