Abstract SEAndroid is deployed on almost all modern Android devices to enforce mandatory access control. The Android Open Source Project regularly publishes a predefined SEAndroid policy that each vendor customises for its devices. These customisations and policy updates may cause security regressions: even small misconfigurations may introduce new information flows leading to exploitable vulnerabilities. We propose a differential verification framework that determines whether security-relevant changes between two SEAndroid configurations affect information-flow properties as intended. Our verification framework is based on the novel comparative modal logic $$ {\text {CML}} $$ CML interpreted over pairs of Kripke structures. We formalise SEAndroid policies within this logic and define a suitable model-checking algorithm for differential reasoning. We implement our framework in the tool Mordente , and evaluate it on real-world SEAndroid policies.

Background Smart contracts are revolutionizing the way two or more parties subscribe to and apply an agreement. The main reason is that they promise to increase efficiency, transparency, and security. However, their inherent vulnerabilities can lead to automated exploits, resulting in significant resource losses. Among these, reentrancy is one of the most impactful security flaws. Over the past few years, reentrancy vulnerabilities have caused substantial financial damage and threatened the viability of entire blockchain ecosystems. Therefore, investigating whether reentrancy can be effectively mitigated and exploring the methodologies designed to address it is crucial. Methodology This paper aims to provide a comprehensive understanding of the impact of reentrancy vulnerabilities in Ethereum smart contracts and to assess the theoretical and practical approaches proposed to counter them. By following the PRISMA framework, we conduct a literature review of academic publications to identify, screen, and analyze relevant studies on detection and mitigation techniques. Results Our findings indicate that the estimated financial loss due to reentrancy attacks amounted to around 350 million USD by 2023, with increasing frequency and profitability of incidents. Despite advancements in mitigation tools, particularly machine learning, they only partially address vulnerabilities and remain ineffective against zero-day attacks. Contribution This paper identifies critical challenges in reentrancy detection, including the lack of standardized benchmarks and data on zero-day vulnerabilities. It emphasizes the need for unified datasets and evaluation frameworks to facilitate fair comparisons, improving detection effectiveness. Additionally, it highlights the need for tools addressing all four reentrancy vulnerability types and reporting performance results.

The increasing digitalization of the space industry and the rapid expansion of commercial space activities have increased the sector’s exposure to cyber threats. As satellite operators and aerospace entities rely on Internet-connected devices (ICDs) for control, communication, and ground-based operations, their attack surface expands accordingly. Despite this growing risk, there remains a lack of standardized methodologies tailored to measuring real-world cybersecurity exposure of ICDs in the space sector. Existing frameworks often overlook the unique characteristics of space infrastructure, including persistent connectivity, long system lifespans, and limited patching opportunities. To address this gap, we propose the Risk Exposure Framework (REF), a methodology to quantify cybersecurity exposure using Internet-facing asset data. REF integrates elements from well-established risk assessment models with targeted analysis of exposed services, known vulnerabilities, and exploit availability. The framework calculates risk through a structured approach that combines Exposure and Likelihood scores based on observable attack surface metrics. Our methodology allows one to compare exposure levels across organizations and supports alignment with sector-specific cybersecurity requirements, and it is adaptable to other critical infrastructure environments where external exposure plays a central role in cyber risk. Unlike general-purpose frameworks, REF directly captures space-specific traits by relying on observable network exposure indicators and by aligning with the principles of attack surface measurement in space environments. REF quantifies the externally observable posture of space organisations, primarily ground-segment and enterprise networks, based on Internet-facing exposure and exploitability. The framework does not model spacecraft constraints, but it can reflect their downstream effects when those constraints manifest at network boundaries. This paper also examines how the REF methodology can support existing cybersecurity policy frameworks and risk assessment strategies in both Europe and the United States.

Parsing and validation functions are crucial because they process untrusted data, e.g., user inputs. Due to their complexity, these functions are highly susceptible to bugs, making them a primary target for security audits. However, identifying such functions within a binary is time-intensive and challenging, given the numerous functions typically present and the lack of source code or supporting documentation. This paper presents an AI-based methodology for identifying functions with parser-like behavior and complex processing logic within a binary. Our methodology analyzes each binary by identifying its functions, extracting their Control Flow Graphs (CFGs), and enriching them with features derived from an embedding model that captures both structural and semantic aspects of their behavior. These annotated CFGs are the input to a Graph Neural Network trained to identify parsing functions. We implement this methodology in the tool ParserHunter, which allows users to train the model on labeled data, query the model with unseen binaries, and accommodate a symbolic execution phase on the processed binary through a user interface. Our experiments on ten real-world projects from GitHub show that our tool effectively identifies parsers in binaries.

People increasingly use digital platforms to exchange resources in accordance with some policies stating what resources users offer and what they require in return. In this paper, we propose a formal model of these environments, focussing on how users' policies are defined and enforced, so ensuring that malicious users cannot take advantage of honest ones. To that end, we introduce the declarative policy language MuAC and equip it with a formal semantics. To determine if a resource exchange is fair, i.e., if it respects the MuAC policies in force, we introduce the non-standard logic MuACL that combines non-linear, linear and contractual aspects, and prove it decidable. Notably, the operator for contractual implication of MuACL is not expressible in linear logic. We define a semantics preserving compilation of MuAC policies into MuACL, thus establishing that exchange fairness is reduced to finding a proof in MuACL. Finally, we show how this approach can be put to work on a blockchain to exchange non-fungible tokens.

In multiagent systems autonomous agents interact with each other to achieve individual and collective goals. Typical interactions concern negotiation and agreement on resource exchanges. Modeling and formalizing these agreements pose significant challenges, particularly in capturing the dynamic behaviour of agents, while ensuring that resources are correctly handled. Here, we propose exchange environments as a formal setting where agents specify and obey exchange policies, which are declarative statements about what resources they offer and what they require in return. Furthermore, we introduce a decidable extension of the computational fragment of linear logic as a fundamental tool for representing exchange environments and studying their dynamics in terms of provability.

The advancement in communications technologies and recent geopolitical events highlighted the need for fast and reliable satellite communications infrastructure for military and civil security operations. Starting from the case study of the Viasat cyberattack in February 2022, this paper analyzes the common vulnerabilities of the ground and, in particular, user segments in SatCom infrastructures, focusing on modems security, and proposes some best practices and solutions in the field of risk management to prevent such attacks. Moreover, the research compares the standards and the guidelines used in the United States concerning routers and network security with those in the European Union. Our findings highlight the need for clear and effective standards or certification schemes to cyber-proof the new components of IRIS2, the “Infrastructure for Resilience Interconnectivity and Security by Satellite”, Europe's first multi-orbital satellite constellation. This need becomes more compelling, especially in view of the entry into force of the Network and Information Security Directive or NIS2 Directive. We conclude by discussing future research directions and emerging trends in cyber risk management for the SatCom user segment. This paper aims to provide valuable insights into managing cyber risks in critical space infrastructure and can inform future efforts to improve cybersecurity in view of IRIS2.

Security Enhanced Linux (SELinux) is a security architecture for Linux implementing Mandatory Access Control. It has been used in numerous security-critical contexts ranging from servers to mobile devices. However, its application is challenging as SELinux security policies are difficult to write, understand, and maintain. Recently, the intermediate language CIL was introduced to foster the development of high-level policy languages and to write structured configurations. Despite CIL’s high level features, CIL configurations are hard to understand as different constructs interact in non-trivial ways. Moreover, there is no mechanism to ensure that a given configuration obeys desired information flow policies. To remedy this, we enrich CIL with a formal semantics, and we propose IFCIL, a backward compatible extension of CIL for specifying fine-grained information flow requirements. Using IFCIL, administrators can express confidentiality, integrity, and non-interference properties. We also provide a tool to statically verify these requirements and we experimentally assess it on ten real-world policies.

Physical layer security mechanisms use primitives that exploit physical properties of the communication channel to protect data. Protecting communications at the physical layer offers some advantages, e.g., in terms of reduced computations, since complex cryptographic procedures are not executed, However, these mechanisms lack a formal specification that prevent protocols and applications that use them from being verified and compared with those based on cyptography. Here we start filling this gap by providing an axiomatization of key physical layer security primitives and proposing a variant of the Dolev–Yao attacker model that takes them into account. We show that our formalization enables applying existing automatic tools for verifying security of protocols. Then, we show that these primitives are a valuable alternative and effective complement to cryptography, because they ensure confidentiality and integrity but require a lower energy consumption and often they also reduce transmission time. Finally, we characterize the specific application domains and network features that make adopting these security mechanisms particularly profitable with respect to the AES cypher.

International audience

Hybrid Casper is the new Ethereum blockchain protocol that uses both Proof of Work and Proof of Stake to reach a consensus between nodes. Here, we analyze the protocol using PRISM+ , an extension of the probabilistic model checker PRISM with primitives for expressing blockchain data types. First, we extend PRISM+ to include data types and operations for modeling and analyzing Proof of Stake based consensus protocols. Then, we model Hybrid Casper in PRISM+ as a parallel composition of stochastic processes, thus precisely describing the behavior of the protocol and highlighting its corner cases. PRISM+ is therefore used to rapidly and automatically analyze the resilience of Hybrid Casper when tuning, up or down, several basic parameters of the protocol, such as the rates of creating blocks, and the strategies for determining penalties. Finally, we study the robustness of Hybrid Casper to two well-known attacks: the Eclipse attack and the majority attack.

Security Enhanced Linux (SELinux) is a security architecture for Linux implementing mandatory access control. It has been used in numerous security-critical contexts ranging from servers to mobile devices. But this is challenging as SELinux security policies are difficult to write, understand, and maintain. Recently, the intermediate language CIL was introduced to foster the development of high-level policy languages and to write structured configurations. However, CIL lacks mechanisms for ensuring that the resulting configurations obey desired information flow policies. To remedy this, we propose IFCIL, a backward compatible extension of CIL for specifying fine-grained information flow requirements for CIL configurations. Using IFCIL, administrators can express, e.g., confidentiality, integrity, and non-interference properties. We also provide a tool to statically verify these requirements.

Firewalls are essential for managing and protecting computer networks. They permit specifying which packets are allowed to enter a network, and also how these packets are modified by IP address translation and port redirection. Configuring a firewall is notoriously hard, and one of the reasons is that it requires using low level, hard to interpret, configuration languages. Equally difficult are policy maintenance and refactoring, as well as porting a configuration from one firewall system to another. To address these issues we introduce a pipeline that assists system administrators in checking if: (i) the intended security policy is actually implemented by a configuration; (ii) two configurations are equivalent; (iii) updates have the desired effect on the firewall behavior; (iv) there are useless or redundant rules; additionally, an administrator can (v) transcompile a configuration into an equivalent one in a different language; and (vi) maintain a configuration using a generic, declarative language that can be compiled into different target languages. The pipeline is based on IFCL, an intermediate firewall language equipped with a formal semantics, and it is implemented in an open source tool called FWS. In particular, the first stage decompiles real firewall configurations for iptables, ipfw, pf and (a subset of) Cisco IOS into IFCL. The second one transforms an IFCL configuration into a logical predicate and uses the Z3 solver to synthesize an abstract specification that succinctly represents the firewall behavior. System administrators can use FWS to analyze the firewall by posing SQL-like queries, and update the configuration to meet the desired security requirements. Finally, the last stage allows for maintaining a configuration by acting directly on its abstract specification and then compiling it to the chosen target language. Tests on real firewall configurations show that FWS can be fruitfully used in real-world scenarios.

Decentralized blockchain platforms have enabled the secure exchange of crypto-assets without the intermediation of trusted authorities. To this purpose, these platforms rely on a peer-to-peer network of byzantine nodes, which collaboratively maintain an append-only ledger of transactions, called blockchain. Transactions represent the actions required by users, e.g. the transfer of some units of crypto-currency to another user, or the execution of a smart contract which distributes crypto-assets according to its internal logic. Part of the nodes of the peer-to-peer network compete to append transactions to the blockchain. To do so, they group the transactions sent by users into blocks, and update their view of the blockchain state by executing these transactions in the chosen order. Once a block of transactions is appended to the blockchain, the other nodes validate it, re-executing the transactions in the same order. The serial execution of transactions does not take advantage of the multi-core architecture of modern processors, so contributing to limit the throughput. In this paper we develop a theory of transaction parallelism for blockchains, which is based on static analysis of transactions and smart contracts. We illustrate how blockchain nodes can use our theory to parallelize the execution of transactions. Initial experiments on Ethereum show that our technique can improve the performance of nodes.

Computer systems often provide hardware support for isolation mechanisms such as privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken, the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features brings a risk of introducing new software-based side-channel attacks. This article studies the problem of extending a processor with new features without weakening the security of the isolation mechanisms that the processor offers. Our solution is heavily based on techniques from research on programming languages. More specifically, we propose to use the programming language concept of full abstraction as a general formal criterion for the security of a processor extension. We instantiate the proposed criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility. This is a very relevant instantiation, as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves and prove that it satisfies our security criterion. We also implement the design on an open-source enclave-enabled microprocessor and evaluate the cost of our design in terms of performance and hardware size.

Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features, brings a risk of introducing new such side-channel attacks. This paper studies the problem of extending a processor with new features without weakening the security of the isolation mechanisms that the processor offers. We propose to use full abstraction as a formal criterion for the security of a processor extension, and we instantiate that criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility of these enclaves. This is a very relevant instantiation as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves, and prove that it satisfies our security criterion. We also implement the design on an open-source enclave-enabled microprocessor, and evaluate the cost of our design in terms of performance and hardware size.

Abstract Verifying the correctness of a system as a whole requires establishing that it satisfies a global specification. When it does not, it would be helpful to determine which modules are incorrect. As a consequence, specification decomposition is a relevant problem from both a theoretical and practical point of view. Until now, specification decomposition has been independently addressed by the control theory and verification communities throughnatural projectionandpartial model checking, respectively. We prove that natural projection reduces to partial model checking and, when cast in a common setting, the two are equivalent. Apart from their foundational interest, our results build a bridge whereby the control theory community can reuse algorithms and results developed by the verification community. Furthermore, we extend the notions of natural projection and partial model checking from finite-state to symbolic transition systems and we show that the equivalence still holds. Symbolic transition systems are more expressive than traditional finite-state transition systems, as they can model large systems, whose behavior depends on the data handled, and not only on the control flow. Finally, we present an algorithm for the partial model checking of both kinds of systems that can be used as an alternative to natural projection.

The Internet of Things (IoT) devices access and process large amounts of data. Some of them are sensitive and can become a target for security attacks. As a consequence, it is crucial being able to trace data and to identify their paths. We start from the specification language IOT-LYSA, and propose a Control Flow Analysis for statically predicting possible trajectories of data communicated in an IoT system and, consequently, for checking whether sensitive data can pass through possibly dangerous nodes. Paths are also interesting from an architectural point of view for deciding which are the points where data are collected, processed, communicated and stored and which are the suitable security mechanisms for guaranteeing a reliable transport from the raw data collected by the sensors to the aggregation nodes and to servers that decide actuations.

Configuring and maintaining a firewall configuration is notoriously hard. Policies are written in low-level, platform-specific languages where firewall rules are inspected and enforced along non trivial control flow paths. Further difficulties arise from Network Address Translation (NAT), since filters must be implemented with addresses translations in mind. In this work, we study the problem of decompiling a real firewall configuration into an abstract specification. This abstract version throws the low-level details away by exposing the meaning of the configuration, i.e., the allowed connections with possible address translations. The generated specification makes it easier for system administrators to check if: (i) the intended security policy is actually implemented; (ii) two configurations are equivalent; (iii) updates have the desired effect on the firewall behavior. The peculiarity of our approach is that is independent of the specific target firewall system and language. This independence is obtained through a generic intermediate language that provides the typical features of real configuration languages and that separates the specification of the rulesets, determining the destiny of packets, from the specification of the platform-dependent steps needed to elaborate packets. We present a tool that decompiles real firewall configurations from different systems into this intermediate language and uses the Z3 solver to synthesize the abstract specification that succinctly represents the firewall behavior and the NAT. Tests on real configurations show that the tool is effective: it synthesizes complex policies in a matter of minutes and, and it answers to specific queries in just a few seconds. The tool can also point out policy differences before and after configuration updates in a simple, tabular form.

The Internet of Things (IoT) offers the infrastructure of the information society. It hosts smart objects that automatically collect and exchange data of various kinds, directly gathered from sensors or generated by aggregations. Suitable coordination primitives and analysis mechanisms are in order to design and reason about IoT systems, and to intercept the implied technological shifts. We address these issues from a foundational point of view. To study them, we define IoT-LySa, a process calculus endowed with a static analysis that tracks the provenance and the manipulation of IoT data, and how they flow in the system. The results of the analysis can be used by a designer to check the behaviour of smart objects, in particular to verify non-functional properties, among which security.

Adaptive systems improve their efficiency by modifying their behaviour to respond to changes in their operational environment. Also, security must adapt to these changes and policy enforcement becomes dependent on the dynamic contexts. We study these issues within [Formula: see text], (the core of) an adaptive declarative language proposed recently. A main characteristic of [Formula: see text] is to have two components: a logical one for handling the context and a functional one for computing. We extend this language with security policies that are expressed in logical terms. They are of two different kinds: context and application policies. The first, unknown a priori to an application, protect the context from unwanted changes. The others protect the applications from malicious actions of the context, can be nested and can be activated and deactivated according to their scope. An execution step can only occur if all the policies in force hold, under the control of an execution monitor. Beneficial to this is a type and effect system, which safely approximates the behaviour of an application, and a further static analysis, based on the computed effect. The last analysis can only be carried on at load time, when the execution context is known, and it enables us to efficiently enforce the security policies on the code execution, by instrumenting applications. The monitor is thus implemented within [Formula: see text], and it is only activated on those policies that may be infringed, and switched off otherwise.

Adaptive systems are designed to modify their behaviour in response to changes of their operational environment. We propose a two-component language for adaptive programming, within the Context-Oriented Programming paradigm. It has a declarative constituent for programming the context and a functional one for computing. We equip our language with a dynamic formal semantics. Since wrong adaptation could severely compromise the correct behaviour of applications and violate their properties, we also introduce a two-phase verification mechanism. It is based on a type and effect system that type-checks programs and computes, as an effect, a sound approximation of their behaviour. The effect is exploited at load time to mechanically verify that programs correctly adapt themselves to all possible running environments.

Type and effect systems significantly extend type systems and allow one to express general semantic properties and to statically reason about programs execution. They have been widely exploited to specify static analyses, for example to track computational side effects, resource usage and communication in concurrent languages. In this paper we adopt abstract interpretation techniques to express type and effect systems as abstract semantics. We extend the Cousot's methodology by introducing an abstract domain which (i) is able to express types with annotations, (ii) is reusable in different analyses with few modifications and (iii) is easily implementable. To test our approach we reconstruct two analyses for which the type and effect systems approach were successful.