OLIVE is a containerized Multi-Factor Authentication (MFA) architecture designed to adapt to diverse security requirements in Vehicle-to-Everything (V2X) communications. By integrating multiple authentication factors, it provides adaptability and scalability to match the required level of security. Beyond the standard three authentication factors, OLIVE supports additional custom factors housed in independent containers. The nature of this modular design and its alignment with current security standards enable efficient resource management while ensuring compatibility with both autonomous and nonautonomous vehicles. OLIVE's adaptability positions it as a versatile solution for various applications, including dynamic Electric Vehicle (EV) charging and zero-trust architectures.

Autonomous Vehicles (AVs) rely on sensor-based perception systems and high-definition maps for navigation. How-ever, their performance may degrade in challenging conditions such as poor visibility, unpredictable traffic conditions, or GNSS-denied environments like urban canyons or temporary construction zones. To address these limitations, we introduce Time-Logic-Map (TLM), a spatial messaging language that enables the road infrastructure to broadcast structured, machine-readable messages to supplement AV perception and support decision-making. This approach reduces the dependence on onboard sensors and describes road logic through machine-oriented language. TLM organizes road information into three layers: map, defining road geometry and a local 3D Cartesian coordinate system; logic, encoding the structural layout of roads and the precedence rules governing vehicle movements; and time, broadcasting real-time information like traffic signal phases. We describe modular design using multiple practical examples in standard and complex intersections, as well as in road construction zones.

Abstract The widespread use of advanced driver assistance systems in modern vehicles, together with their integration with the Internet and other road nodes, has made vehicle more vulnerable to cyber-attacks. To address these risks, the automotive industry is increasingly focusing on the development of security solutions: formal methods and software verification techniques, which have been successfully applied to a number of safety-critical systems, could be a promising approach in the automotive area. In this work, we concentrate on in-vehicle communications, provided by many Electronic Control Units (ECUs) that work together thanks to serial protocols such as Controller Area Network (CAN). However, increasing connectivity exposes the internal network to a variety of cyber-risks. Our aim is to formally verify the AUTOSAR-based Basic Software module called CINNAMON, designed to ensure confidentiality, integrity, and authentication at the same time for traffic exchanged over CAN protocol. More precisely, it adds confidentiality guarantees to the Secure Onboard Communication (SecOC) module. We formally analyze CINNAMON with the verification tool Tamarin. Our analysis shows that CINNAMON could be an effective security solution, as it can ensure the desired properties, in particular, confidentiality in a send-receive scenario between two ECUs. Finally, we describe a potential application scenario.

In recent years, the automotive industry has undergone a revolution in which data has become one of the most important element of vehicle functionality. However, most of the in-vehicle networking paradigms have limitations in accommodating this data surge. To address this need, Automotive Ethernet (AE) has emerged as a promising solution. Concurrently, there is an urgent demand to guarantee data security and privacy within vehicle networks by designing ad hoc vehicular solutions. For this reason, our study undertakes the design and evaluation of four distinct ISO/OSI layer 2 security configurations, here named profiles, tailored to AE. By leveraging advanced security techniques such as MACsec and SecOC-related solutions, these profiles are engineered to ensure robust data confidentiality, integrity, and authenticity. To assess their efficacy, we created a testbed with Raspberry units to emulate an in-vehicle environment. We carried out a comprehensive timing analyses to uncover the performance attributes of each solution. We aim to provide insights for the development of secure and efficient data communication systems within the in-vehicle networks.

In recent years, data can be considered the new fuel for road vehicle functionalities like driver-assistance systems or customized services. Therefore, the carmakers with their phone apps, synced with the infotainment system, can collect information from the drivers and vehicles to be processed inside or outside the car. In this context, we analyze different carmakers’ privacy policies to define their readability and compliance with the EU General Data Protection Regulation, and provide analysis of carmakers’ data collection. Besides, for the first time, we compare the most significant privacy regulations in automotive. Finally, we create an interactive dashboard to compare the different carmakers’ policies and provide users with an efficient instrument to understand some relevant privacy aspects like which data the carmakers declare to collect. We find that carmakers could collect a large number of users and vehicle data, but, in some cases, the privacy policies seem to be quite challenging to read and do not provide some information like how collected data are protected or stored.

Over the next few years, the automotive industry is set to experience a revolutionary transformation driven by several interconnected trends such as autonomous driving, connected vehicles, and electrification. Our research focuses on Software-Defined Vehicles (SDVs), their definition, and an analysis of their possible cybersecurity issue. SDV is a new concept that is changing the definition of vehicles from purely hardware-based to software-oriented. The research analyzes the SDV security following the ISO/SAE 21434 guidelines, performing a complete vulnerability assessment to determine the main possible threats and their impact on different aspects like safety and operations. The findings suggest that SDVs may be the future of the automotive industry and will offer greater convenience and sustainability, throughout the vehicle life cycle but only if appropriate solutions to mitigate potential security threats like denial-of-service or jamming attacks, will be implemented.

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.

We present the link-calculus, an extension of π-calculus, that models interactions that are multiparty, i.e. that may involve more than two processes, mutually exchanging data. Communications are seen as chains of suitably combined links (which record the source and the target ends of each hop of interactions), each contributed by one party. Values are exchanged by means of message tuples, still provided by each party. We develop semantic theories and proof techniques for link-calculus and apply them in reasoning about complex distributing computing scenarios, where more than two participants need to synchronise in order to perform a task. In particular, we introduce the notion of linked bisimilarity in analogy with the early bisimilarity of the π-calculus. Differently from the π-calculus case, we can show that it is a congruence with respect to all the link-calculus operators and that is also closed under name substitution.

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.

A type flaw attack on a security protocol is an attack where an honest principal is cheated on interpreting a field in a message as the one with a type other than the intended one. In this paper, we shall present an extension of the LYSA calculus to cope with types, by using tags to represent the i ntended types of terms. We develop a Control Flow Analysis for this calculus which soundly over-approximates all the possible behaviour of a protocol and, in particular, is able to capture any type confusion that may occur during the protocol execution. The analysis acts in a descriptive way: it describes which violations may occur. In the same setting, our approach also offers a prescriptive usage: we can impose a type discipline, by forcing some data to be of the expected types. At this point, the analysis may statically check that type violations are not possible any longer. In other words, we instrument the code with the only checks necessary to enforce type security. Finally, we apply our framework to a multi-protocol setting, where the risk of having type flaw attacks is higher. Our analysis has been implemented and successfully applied to a number of security protocols, showing it is able to capture type flaw attacks. The implementation complexity of the analysis is low polynomial.

BACKGROUND: Metabolic networks present a complex interconnected structure, whose understanding is in general a non-trivial task. Several formal approaches have been developed to support the investigation of such networks. One of the relevant problems in this context is the comprehension of causality dependencies amongst the molecules involved in the metabolic process. RESULTS: We apply techniques from formal methods and computational logic to develop an abstract qualitative model of metabolic networks in order to determine possible causal dependencies. Keeping in mind both expressiveness and ease of use, we aimed at providing: i) a minimal notation to represent causality in biochemical interactions, and ii) an automated tool allowing human experts to easily vary conditions of in silico experiments. We exploit a reading of chemical reactions in terms of logical implications: starting from a description of a metabolic network in terms of reaction rules and initial conditions, chains of reactions, causally depending one from the another, can be automatically deduced. Both the components of the initial state and the clauses ruling reactions can be easily varied and a new trial of the experiment started, according to a what-if investigation strategy. Our approach aims at exploiting computational logic as a formal modeling framework, amongst the several available, that is naturally close to human reasoning. It directly leads to executable implementations and may support, in perspective, various reasoning schemata. Indeed, our abstractions are supported by a computational counterpart, based on a Prolog implementation, which allows for a representation language closely correspondent to the adopted chemical abstract notation. The proposed approach has been validated by results regarding gene knock-out and essentiality for a model of the metabolic network of Escherichia coli K12, which show a relevant coherence with available wet-lab experimental data. CONCLUSIONS: Starting from the presented work, our goal is to provide an effective analysis toolkit, supported by an efficient full-fledged computational counterpart, with the aim of fruitfully driving in vitro experiments by effectively pruning non promising directions.

We methodically expand protocol narrations into terms of a process algebra in order to specify some of the checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols.

We introduce a Control Flow Analysis that statically approximates the dynamic behaviour of mobile processes, expressed in (a variant of) the π-calculus. Our analysis of a system is able to describe the essential behaviour of each sub-system, tracking

We perform a systematic expansion of protocol narrations into terms of process algebra in order to make precise some of the detailed checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice for identifying a number of authentication flaws in symmetric key protocols such as Needham-Schroeder, Otway-Rees, Yahalom and Andrew Secure RPC.

We address the problem of message authentication using the /spl pi/-calculus, which has been given an operational semantics that provides each sequential process of a system with its own local space of names. We exploit here that semantics and its localized names to guarantee by construction that a message has been generated by a given entity. Therefore, our proposal can be seen as a reference for the analysis of "real" protocols. As an example, we study the way authentication is ensured by encrypting messages in the spi-calculus.