The FDO protocol is the leading candidate to become the reference standard for automatic device onboarding. However, as documented in the literature, it may suffer from a security issue exploiting its Ownership Voucher when the supply chain of the device cannot be considered trusted. In a previous work, we showed a possible attack of this type, found by performing a formal analysis on a symbolic model of the protocol. The first contribution of this paper is to present the analysis done in the previous work in a more comprehensive way, to extend it, and to show that the attack found is also possible on a real implementation of the protocol. We then analyse some possible solutions proposed in the literature as countermeasures to try to mitigate the attack. After demonstrating that they may not completely solve the mentioned issue, we propose our own solution, which could be taken into consideration by the FIDO Working Group to further improve the protocol specification. Again, as a demonstration of the logical correctness of our solution, we formally analyse its symbolic model.

The increasing complexity and size of virtual networks, jointly with the fast-evolving nature of modern threats, have significantly amplified the challenge of mitigating cyberattacks in real time. In particular, these factors have made the traditional approaches for network security reconfiguration unfeasible, as they rely heavily on manual operations. To address these issues, this demo presents a looping process that autonomously mitigates ongoing attacks by extracting security policies from intrusion detection system alerts and automatically reconfiguring distributed firewalls via a provably correct and optimized approach. The proposed system architecture is composed of several interconnected components responsible for the full lifecycle from the detection of an attack to the deployment of the updated and secure configuration, operating in a fully automated and self-triggering way, aiming to reduce human involvement while improving mitigation speed and correctness.

Vehicle-to-Everything (V2X) communications are expected to reshape road mobility in the increasingly near future. This type of communication allows a vehicle to transmit information, such as its position and speed, which can be used for different applications. However, despite the benefits, the increased connectivity and data sent over the network may expose the vehicle to a significant number of cyber attacks. This paper takes one of the schemes proposed in the literature to protect the security and privacy of the vehicles, and analyses it from a security and privacy perspective using Proverif. Specifically, this scheme is unique in combining asymmetric encryption with digital certificates and group signatures used by vehicles to self-certify those certificates. We present a formal model able to capture all the main aspects of the protocol and the context in which it works, and show how security and privacy properties can be expressed for formal verification in Proverif. Our analysis conducted on the model of the protocol revealed some weaknesses for which we tried to provide a solution.

Nowadays, the security management of packet filtering firewall policies got complicated due to the evolution of modern computer networks, characterized by growing size and heterogeneity of communications. The traditional manual approaches for configuring firewalls have become error-prone, unoptimized and time-consuming, leading to an increasing number of policy anomalies, including both sub-optimizations and conflicts. In literature, the techniques proposed for anomaly management have several shortcomings, as their anomaly analysis is usually excessively complex, while their anomaly resolution cannot solve all anomalies. In order to overcome these shortcomings, this article proposes a comprehensive approach for firewall policy anomaly analysis and resolution, based on the formal concept of atomic predicates. This approach has the aim to simplify the anomaly management operations, make them efficient and solve all configuration anomalies. The achievement of these objectives has been experimentally proved through the validation of a framework which implements the proposed approach, and whose time performance and anomaly management efficiency have been compared with the relevant alternative approaches.

The configuration of security systems for communication protection, such as VPNs, is traditionally performed manually by human beings. However, because the complexity of this task becomes soon difficult to manage when its size increases, critical errors that may open the door to cyberattacks may be introduced. Moreover, even when a solution is computed correctly, sub-optimizations that may afflict the performance of the configured VPNs may be introduced. Unfortunately, the possible solution that consists in automating the definition of VPN configurations has been scarcely studied in literature so far. Therefore, this paper proposes an automatic approach to compute the configuration of VPN systems. Both the allocation scheme of VPN systems in the network and their protection rules are computed automatically. This result is achieved through the formulation of a Maximum Satisfiability Modulo Theories problem, which provides both formal correctness-by-construction and optimization of the result. A framework implementing this approach has been developed, and its experimental validation showed that it is a valid alternative for replacing time-consuming and error-prone human operations for significant problem sizes.

Cloud computing has transformed the landscape of application delivery, offering an enormous pool of devices with a wide-spread geographical distribution. In this context, liquid computing is a novel paradigm that aims to avoid that available resources are underutilized, by facilitating their seamless sharing among different tenants and administrative domains. Nevertheless, liquid computing introduces new security challenges, particularly related to network isolation, which traditional approaches are inadequate to address. Therefore, this paper proposes a security orchestrator to automate the configuration of network isolation primitives across a multi-domain and multi-tenant cloud environment, simplifying the implementation of security patterns like zero trust and least privilege. The proposed solution is intent-driven, because users define their requirements in terms of desired and prohibited network communications through a user-friendly language. In our implemented proposal, intents expressed by different users are harmonized to avoid discordances among them, and then they are translated into Kubernetes Network Policies as isolation primitives.

The continuous innovation in network softwarization has enabled higher dynamism and responsiveness in creating and deploying complex network configurations. Following this trend, several approaches have been proposed to automate the allocation and configuration of network security functions to satisfy a set of network security policies, describing the security requirements to be fulfilled in the network. In particular, many studies focused on addressing this problem for the packet filtering firewall, as it is the most common firewall technology used in computer networks. However, those proposed techniques for automatic firewall configuration are not optimized for reconfiguring an already deployed network. This results in a computation delay that is incompatible with the needs of modern networks and the timing of current network attacks. In order to overcome these limitations, this paper proposes an efficient method to reduce the computation time for reconfiguration while providing an automated, formally correct, and optimal placement and configuration of the required network security functions. The proposal has undergone validation and evaluation tests, to show the improvements in comparison to non-optimized approaches.

In the next generation networks and cloud systems, administrators should only need to define their intentions through simple high-level intents, leaving the system to autonomously implement them in the best way possible. The adoption of automation enables the possibility to create reactive systems that can reconfigure themselves in response to unpredictable events, such as network attacks. Nowadays, such solutions are far from being achieved. The enforcement of security requirements continues to heavily rely on manual efforts and tools requiring non-negligible expertise to be used. This results in frequent misconfiguration errors or the complete absence of default security measures due to their high implementation complexity. This paper introduces the research that will be carried out within my Ph.D. program, focusing on network security automation. The objective is to bridge existing gaps in the literature, on one side developing novel automated and intent-based approaches for security enforcement in cloud environments, ensuring formal correctness and optimization, and on the other side researching new solutions for the design of security reaction mechanisms for modern networks in response to network attacks.

Introducing formal methods in the automatic resolution of network security management problems can guarantee solution correctness, so also boosting human confidence in using automatic techniques. A necessary step to achieve this feature is the definition of formal network models, representing network topology, traffic flows, etc. Each state-of-the-art formal network modeling approach has been proposed and validated only for a specific management problem (e.g., verification of configurations or refinement of policies into configurations). This paper analyzes a possible combination of the most promising state-of-the-art modeling approaches into a unified formal model that can be used by existing automatic resolution algorithms to solve both the verification and the refinement problems, without the need of major changes. The model is flexible enough to allow different aggregation levels of traffic into flows. The paper analyzes two opposite flow aggregation strategies, named Atomic Flows and Maximal Flows, and compares their performance when applied to the two identified security problems.

Nowadays, security automation exploits the agility characterizing network virtualization to replace the traditional error-prone human operations. This dynamism allows user-specified high-level intents to be rapidly refined into the concrete configuration rules which should be deployed on virtual security functions. In this revolutionary context, this paper proposes the demonstration of a novel security framework based on an optimized approach for the automatic orchestration of virtual distributed firewalls. The framework provides formal guarantees for the firewall configuration correctness and minimizes the size of the firewall allocation scheme and rule set. The framework produces rules that can be deployed on multiple types of real virtual function implementations, such as iptables, eBPF firewalls and Open vSwitch.

Nowadays virtual computer networks are characterized by high dynamism and complexity. However, these features made the traditional manual approaches for network security management error-prone, unoptimized and time-consuming. This paper discusses the research carried out during my Ph.D. program on network security automation. In particular, it presents an approach based on constraint programming that combines automation, formal verification, and optimization for network security management. This approach has been proved to be general enough by means of multiple applications that have been developed. In particular, this paper describes VEREFOO, a framework for the automatic configuration of security functions, and FATO, a framework for the automatic orchestration of security transients. This methodology is extensively evaluated using different metrics and tests, and it has been compared to state-of-the-art solutions and to the requirements of dynamic virtual networks.

Network virtualization has revolutionized the traditional approaches for security configuration. If in the past error-prone and unoptimized manual operations were performed by human beings, nowadays automated methodologies are employed for establishing the configuration of virtual security functions that can enforce the requested security properties. However, these techniques can only perform the automatic configuration of a single function type at a time. This restriction may be excessively limiting, because the configuration of some functions may directly impact others, and they cannot be configured in sequence. In light of these considerations, the paper investigates the stated problem for the two most commonly used security functions, packet filtering firewalls and channel protection systems. It also proposes a preliminary approach to automatically perform their joint intent-based configuration, by defining the problem through a Maximum Satisfiability Modulo Theories formulation.

In the latest years, multi-domain Kubernetes architectures composed of multiple clusters have been getting more frequent, so as to provide higher workload isolation, resource availability flexibility and scalability for application deployment. However, manually configuring their security may lead to inconsistencies among policies defined in different clusters, or it may require knowledge that the administrator of each domain cannot have. Therefore, this paper proposes an automatic approach for the automatic generation of the network security policies to be deployed in each cluster of a multi-domain Kubernetes deployment. The objectives of this approach are to reduce of configuration errors that human administrators commonly make, and to create transparent cross-cluster communications. This approach has been implemented as a framework named Multi-Cluster Orchestrator, which has been validated in realistic use cases to assess its benefits to Kubernetes orchestration.

The incessant growth of network virtualization determined the proliferation of Virtual Network Functions (VNFs), software programs that can run on general-purpose servers and that can also integrate security controls for protection from cyber-attacks. However, a high availability of VNFs may be counterproductive for the network administrators who have to select the most suitable ones to establish the security configuration of their network. On the one hand, the vendor-dependent technicalities of each VNF may cloud the security controls it can actually perform. On the other hand, VNF selection traditionally occurs before the synthesis of the virtual network graph, so it does not employ any network information and it may outcome unoptimized results. In light of these shortcomings, this paper proposes a novel security configuration workflow, based on new abstractions that we call projections. They represent the security-related operations that VNFs should perform to enforce a security policy. Thanks to these abstractions, the actual selection of the VNFs can be postponed to the moment their deployment in the physical network is actually required. In fact, projections are enough for the synthesis of the virtual security graph. This paper also proposes a two-step algorithm for computing projection chains as candidate solutions for graph synthesis. The proposed approach has been implemented as a Java framework and a set of tests have validated its applicability to real-world VNFs, correctness, scalability and optimization. These tests showed that the new security configuration workflow can achieve a significant reduction for the number of selected VNFs and their deployment cost. Specifically, in the analyzed scenario, the improvement percentages for these two parameters are 79% and 90% with respect to the worst-case strategy, while 68% and 77% with respect to a traditional more optimized configuration strategy.

The configuration of security functions in computer networks is still typically performed manually, which likely leads to security breaches and long re-configuration times. This problem is exacerbated for modern networks based on network virtualization, because their complexity and dynamics make a correct manual configuration practically unfeasible. This article focuses on packet filters, i.e., the most common firewall technology used in computer networks, and it proposes a new methodology to automatically define the allocation scheme and configuration of packet filters in the logical topology of a virtual network. The proposed method is based on solving a carefully designed partial weighted Maximum Satisfiability Modulo Theories problem by means of a state-of-the-art solver. This approach formally guarantees the correctness of the solution, i.e., that all security requirements are satisfied, and it minimizes the number of needed firewalls and firewall rules. This methodology is extensively evaluated using different metrics and tests on both synthetic and real use cases, and compared to the state-of-the-art solutions, showing its superiority.

he growing trend towards network “softwarization” allows the creation and deployment of even complex network environments in a few minutes or seconds, rather than days or weeks as required by traditional methods. This revolutionary approach made it necessary to seek automatic processes to solve network security problems. One of the main issues in the automation of network security concerns the proper and efficient modeling of network traffic. In this paper, we describe two optimized Traffic Flows representation models, called Atomic Flows and Maximal Flows. In addition to the description, we have validated and evaluated the proposed models to solve two key network security problems - security verification and automatic configuration - showing the advantages and limitations of each solution.

Network virtualization increased the versatility in enforcing security protection, by easing the development of new security function implementations. However, the drawback of this opportunity is that a security provider, in charge of configuring and deploying a security function graph, has to choose the best virtual security functions among a pool so large that makes manual decisions unfeasible. In light of this problem, the paper proposes a novel approach for synthesizing virtual security services by introducing the functionality abstraction. This new level of abstraction allows to work in the virtual level without considering the different function implementations, with the objective to postpone the function selection jointly with the deployment, after the configuration of the virtual graph. This novelty enables to optimize the function selection when the pool of available functions is very large. A framework supporting this approach has been implemented and it showed adequate scalability for the requirements of modern virtual networks.

The increased flexibility and interconnectivity of modern industrial communication networks, obtained through the use of innovative technologies like network function virtualization and software-defined networking, require a secure and manageable framework to support the new communication and computing needs. To focus on these requirements, this article proposes a framework for reliable placement of services across physically separated locations, which offers both system optimization, in terms of latency and resource utilization, and connectivity policy enforcement to guarantee service reliability, safety, and security. This is achieved by exploiting a new approach to solve the virtual network embedding problem, using optimization modulo theories (MaxSMT), which allows the use of very expressive constraints.

Network Function Virtualization (NFV) and Software Defined Networking (SDN) are new emerging paradigms that changed the rules of networking, shifting the focus on dynamicity and programmability. In this new scenario, a very important and challenging task is to detect anomalies in the data plane, especially with the aid of suitable automated software tools. In particular, this operation must be performed within quite strict times, due to the high dynamism introduced by virtualization. In this article, we propose a new network modeling approach that enhances the performance of formal verification of reachability policies, checked by solving a Satisfiability Modulo Theories (SMT) problem. This performance improvement is motivated by the definition of function models that do not work on single packets, but on packet classes. Nonetheless, the modeling approach is comprehensive not only of stateless functions, but also stateful functions such as NATs and firewalls. The implementation of the proposed approach achieves high scalability in complex networked systems consisting of several heterogeneous functions.

The rise of new forms of cyber-threats is mostly due to the extensive use of virtualization paradigms and the increasing adoption of automation in the software life-cycle. To address these challenges we propose an innovative framework that leverages the intrinsic programmability of the cloud and software-defined infrastructures to improve the effectiveness and efficiency of reaction mechanisms. In this paper, we present our contributions with a demonstrative use case in the context of Kubernetes. By means of this framework, developers of cybersecurity appliances will not have any more to care about how to react to events or to struggle to define any possible security tasks at design time. In addition, automatic firewall ruleset generation provided by our framework will mostly avoid human intervention, hence decreasing the time to carry out them and the likelihood of errors. We focus our discussions on technical challenges: definition of common actions at the policy level and their translation into configurations for the heterogeneous set of security functions by means of a use case.

Emerging technologies such as Software-Defined Networking and Network Functions Virtualization are making the definition and configuration of network services more dynamic, thus making automatic approaches that can replace manual and error-prone tasks more feasible. In view of these considerations, this paper proposes a novel methodology to automatically compute the optimal allocation scheme and configuration of virtual firewalls within a user-defined network service graph subject to a corresponding set of security requirements. The presented framework adopts a formal approach based on the solution of a weighted partial MaxSMT problem, which also provides good confidence about the solution correctness. A prototype implementation of the proposed approach based on the z3 solver has been used for validation, showing the feasibility of the approach for problem instances requiring tens of virtual firewalls and similar numbers of security requirements.

Distributed systems are extremely difficult to design and implement correctly because they must handle both system correctness and device failures. Most of the work focuses on the first aspect, and in particular, on the correctness of security and network configuration. The large demand for availability and reliability for critical services is actually pushing new architectures that tolerate faults, but a-priori analysis of redundancy and recovery features is still limited. To this end, we present a framework to design and formally verify the persistence of network properties, even in case of failures. The solution considers both nodes and links failure, and it is based on a formal model that takes both network topology and network device configurations into account. In contrast, most of the existing approaches only consider network topology. By analyzing the formal model, the framework can check whether the specified network services are still available after failures, and in case of success, it outputs a possible configuration of the devices to be used for automatic recovery.

Traffic monitoring is essential to manage large networks and validate Service Level Agreements. Passive monitoring is particularly valuable to promptly identify transient fault episodes and react in a timely manner. This article proposes a novel, non-invasive and flexible method to passively monitor large backbone networks. By using only packet counters, commonly available on existing hardware, we can accurately measure packet losses, in different segments of the network, affecting only specific flows. We can monitor not only end-to-end flows, but any generic flow with packets following several different paths in the network (multipoint flows). We also sketch a possible extension of the method to measure average one-way delay for multipoint flows, provided that the measurement points are synchronized. Through various experiments we show that the method is effective and enables easy zooming in on the cause of packet losses. Moreover, the method can scale to very large networks with a very low overhead on the data plane and the management plane.

Abstract Designing and coding security protocols is an error prone task. Several flaws are found in protocol implementations and specifications every year. Formal methods can alleviate this problem by backing implementations with rigorous proofs about their behavior. However, formally-based development typically requires domain specific knowledge available only to few experts and the development of abstract formal models that are far from real implementations. This paper presents a Java-based protocol design and implementation framework, where the user can write a security protocol symbolic model in Java, using a well defined subset of the language that corresponds to applied π -calculus. This Java model can be symbolically executed in the Java debugger, formally verified with ProVerif, and further refined to an interoperable Java implementation of the protocol. Soundness theorems are provided to prove that, under some reasonable assumptions, a simulation relation relates the Java refined implementation to the symbolic model verified by ProVerif, so that, for the usual security properties, a property verified by ProVerif on the symbolic model is preserved in the Java refined implementation. The applicability of the framework is evaluated by developing an extensive case study on the popular SSL protocol.

Network Function Virtualization (NFV) architectures are emerging to increase networks flexibility. However, this renewed scenario poses new challenges, because virtualized networks, need to be carefully verified before being actually deployed in production environments in order to preserve network coherency (e.g., absence of forwarding loops, preservation of security on network traffic, etc.). Nowadays, model checking tools, SAT solvers, and Theorem Provers are available for formal verification of such properties in virtualized networks. Unfortunately, most of those verification tools accept input descriptions written in specification languages that are difficult to use for people not experienced in formal methods. Also, in order to enable the use of formal verification tools in real scenarios, vendors of Virtual Network Functions (VNFs) should provide abstract mathematical models of their functions, coded in the specific input languages of the verification tools. This process is error-prone, time-consuming, and often outside the VNF developers' expertise. This paper presents a framework that we designed for automatically extracting verification models starting from a Java based representation of a given VNF. It comprises a Java library of classes to define VNFs in a more developer-friendly way, and a tool to translate VNF definitions into formal verification models of different verification tools.

Finite state automata (FSA) are used by many network processing applications to match complex sets of regular expressions in network packets. In order to make FSA-based matching possible even at the ever-increasing speed of modern networks, multi-striding has been introduced. This technique increases input parallelism by transforming the classical FSA that consumes input byte by byte into an equivalent one that consumes input in larger units. However, the algorithms used today for this transformation are so complex that they often result unfeasible for large and complex rule sets. This paper presents a set of new algorithms that extend the applicability of multi-striding to complex rule sets. These algorithms can transform nondeterministic finite automata (NFA) into their multi-stride form with reduced memory and time requirements. Moreover, they exploit the massive parallelism of graphical processing units for NFA-based matching. The final result is a boost of the overall processing speed on typical regex-based packet processing applications, with a speedup of almost one order of magnitude compared to the current state-of-the-art algorithms.

Long Term Evolution (LTE) is the most recent standard in mobile communications, introduced by 3rd Generation Partnership Project (3GPP). Most of the formal security analysis works in literature about LTE analyze authentication procedures, while interoperability is far less considered. This paper presents a formal security analysis of the interoperability procedures between LTE and the older Universal Mobile Telecommunications System (UMTS) networks, when mobile devices seamlessly switch between the two technologies. The ProVerif tool has been used to conduct the verification. The analysis shows that security properties (secrecy of keys, including backward/forward secrecy, immunity from off-line guessing attacks and network components authentication) hold almost as expected, if all the protections allowed by the LTE standard are adopted. If backhauling traffic is not protected with IPSec, which is a common scenario since the use of IPSec is not mandatory, some security properties still hold while others are compromised. Consequently, user's traffic and network's nodes are exposed to attacks in this scenario.

In-network function chaining often involves the deployment of multiple applications into a single, possibly multi-tenant, middlebox. This approach has gained much interest since new network paradigms, such as Software Defined Networking (SDN) and Network Function Virtualization (NFV), have been proposed to virtualize resources as well as network functions. In this scenario, it is very common to move data (e.g., packets) from an application to another by means of a switching module that is in charge of chaining network functions in the correct order, also ensuring an adequate level of isolation between any two virtualized components. With this purpose in mind, this paper proposes an efficient algorithm to handle the communication between the internal soft-switch and the heterogeneous network functions that are executed on the same server. Our proposal is designed with the aim of dealing with high speed packet processing, hence an extensive performance evaluation is also provided to prove the goodness of our solution in this context.

Abstract Automated formal verification of security protocols has been mostly focused on analyzing high-level abstract models which, however, are significantly different from real protocol implementations written in programming languages. Recently, some researchers have started investigating techniques that bring automated formal proofs closer to real implementations. This paper surveys these attempts, focusing on approaches that target the application code that implements protocol logic, rather than the libraries that implement cryptography. According to these approaches, libraries are assumed to correctly implement some models. The aim is to derive formal proofs that, under this assumption, give assurance about the application code that implements the protocol logic. The two main approaches of model extraction and code generation are presented, along with the main techniques adopted for each approach.

Abstract When using formal methods, security protocols are usually modeled at a high level of abstraction. In particular, data encoding and decoding transformations are often abstracted away. However, if no assumptions at all are made on the behavior of such transformations, they could trivially lead to security faults, for example leaking secrets or breaking freshness by collapsing nonces into constants. In order to address this issue this paper formally states sufficient conditions, checkable on sequential code, such that if an abstract protocol model is secure under a Dolev–Yao adversary, then a refined model, which takes into account a wide class of possible implementations of the encoding/decoding operations, is implied to be secure too under the same adversary model. The paper also indicates possible exploitations of this result in the context of methods based on formal model extraction from implementation code and of methods based on automated code generation from formally verified models.

Multistride automata speed up input matching because each multistriding transformation halves the size of the input string, leading to a potential 2× speedup. However, up to now little effort has been spent in optimizing the building process of multistride automata, with the result that current algorithms cannot be applied to real-life, large automata such as the ones used in commercial IDSs, because the time and the memory space needed to create the new automaton quickly becomes unfeasible. In this paper, new algorithms for efficient building of multistride NFAs for packet inspection are presented, explaining how these new techniques can outperform the previous algorithms in terms of required time and memory usage.

This paper presents JavaSPI, a "model-driven" development framework that allows the user to reliably develop security protocol implementations in Java, starting from abstract models that can be verified formally. The main novelty of this approach stands in the use of Java as both a modeling language and the implementation language. By using the SSL handshake protocol as a reference example, this paper illustrates the JavaSPI framework.

During last years, the importance of safety aspects in industry has significantly increased. System engineering modeling language SysML is widely used in order to manage increasing complexity of embedded systems. Being just a modeling language, SysML does not provide integrated means of verification and validation for its models. Therefore, additional efforts are needed for checking consistency of models. This work shows efforts towards integrating embedded systems modeling with verification measures, namely, with refinement checking (checking whether a system description is really an implementation of another, more abstract, system description) applied to statemachines linked to SysML requirements. We show how such verification can be done automatically with the help of externally implemented tools.

As fieldbus networks are becoming accessible from the Internet, security mechanisms to grant access only to authorized users and to protect data are becoming essential. This paper proposes a formally based approach to the analysis of such systems, both at the security protocols level and at the system architecture level. This multilevel analysis allows the evaluation of the effects of an attack on the overall system, due to security problems that affect the underlying security protocols. A case study on a typical fieldbus security system validates the approach.

We propose a stateless packet filtering technique based on finite-state automata (FSA). FSAs provide a comprehensive framework with well-defined composition operations that enable the generation of stateless filters from high-level specifications and their compilation into efficient executable code without resorting to various opportunistic optimization algorithms. In contrast with most traditional approaches, memory safety and termination can be enforced with minimal run-time overhead even in cyclic filters, thus enabling full parsing of complex protocols and supporting recursive encapsulation relationships. Experimental evidence shows that this approach is viable and improves the state of the art in terms of filter flexibility, performance, and scalability without incurring in the most common FSA deficiencies, such as state-space explosion.

We report on our experience with the formal verification of CalRoc2003, the software that controls the scientific payload for the SCORE coronographic experiment. Our target was using the state-of-the-art SPIN model checker for spotting concurrency problems that could have gone undetected in the traditional testing phase. Some challenges had to be faced in this task. Since the software interacts heavily with the operating system for inter-process communication and process management, the relevant OS primitives had to be modelled. Moreover, since CalRoc2003 is written in C++, the automatic model extraction tools coming with SPIN are inapplicable because they only target C programs, and models had to be extracted manually. Even with these difficulties, the verification proved useful in detecting some subtle problems in the software.

In modern factories, personal computers are starting to replace traditional programmable logic controllers, due to cost and flexibility reasons, and also because their operating systems now support programming environments even suitable for demanding real-time applications. These characteristics, as well as the ready availability of many software packages covering any kind of needs, have made the introduction of PC-based devices at the factory field level especially attractive. However, this approach has a profound influence on the extent of threats that a factory computing infrastructure shall be prepared to deal with. In fact, industrial personal computers share the same kinds of vulnerabilities with their office automation counterparts. Then, their introduction increases the risk of cyber-attacks. As the complexity of the network grows, the problem rapidly becomes hard to tackle by hand, due to the subtle and unforeseen interactions that may occur among apparently unrelated vulnerabilities, thus bearing the focus on the full automation of the analysis. Going into this direction, this paper presents a software tool that, given an accurate and machine-readable description of vulnerabilities, detects whether or not they are of concern and evaluates consequences in the context of a factory network.

In formal methods, security protocols are usually modeled with a high level of abstraction. In particular, marshalling/unmarshalling operations on transmitted messages are generally abstracted away. However, in real applications, errors in this protocol component could be exploited to break protocol security. In order to solve this issue, this paper formally shows that, under some constraints checkable on sequential code, if an abstract protocol model is secure, then a refined model, which takes into account a wide class of possible implementations of the marshalling/unmarshalling operations, is implied to be secure too. The paper also indicates possible exploitations of this result.

This paper describes the design and implementation of a lightweight static security analyzer that exploits the compilation process of the gcc compiler. The tool is aimed at giving to programmers useful and precise hints for improving the security of the developed software, while also detecting format string vulnerabilities, buffer overflows, and subtle vulnerabilities due to incorrect arithmetic and conversion on integers. The experimented technique is a combination of the taint analysis concept and of a value range propagation algorithm. The experimental results obtained by analyzing some real-world security critical programs show that the tool is only slightly heavier than pure compilation, and that it is able to detect known vulnerabilities, as well as unknown ones. Moreover, even if false positives are given, many of the warnings that do not correspond to vulnerabilities are indeed instances of unsafe programming practices, which can be avoided by applying a defensive programming style. Then, the tool can be profitably used during development, as a means that facilitates such coding practice.

Abstract This paper addresses the problem of representing the intruder’s knowledge in the formal verification of cryptographic protocols, whose main challenges are to represent the intruder’s knowledge efficiently and without artificial limitations on the structure and size of messages. The new knowledge representation strategy proposed in this paper achieves both goals and leads to practical implementation because it is incrementally computable and is easily amenable to work with various term representation languages. In addition, it handles associative and commutative term composition operators, thus going beyond the free term algebra framework. An extensive computational complexity analysis of the proposed representation strategy is included in the paper.

Spi2Java is a tool that enables semi-automatic generation of cryptographic protocol implementations, starting from verified formal models. This paper shows how the last version of spi2Java has been enhanced in order to enable interoperability of the generated implementations. The new features that have been added to spi2Java are reported here. A case study on the SSH transport layer protocol, along with some experiments and measures on the generated code, is also provided. The case study shows, with facts, that reliable and interoperable implementations of standard security protocols can indeed be obtained by using a code generation tool like spi2Java.

The aim of this work is to describe a tool (Spi2Java) that automatically generates Java code implementing cryptographic protocols described in the formal specification language spi calculus. Spi2Java is part of a set of tools for spi calculus, also including a preprocessor, a parser, and a security analyzer. The latter can formally analyze protocols and detect protocol flaws. When a protocol has been analyzed and an adequate confidence about its correctness has been reached, Spi2Java can generate a corresponding correct Java implementation of the protocol, thus dramatically reducing the risk of introducing security flaws in the coding phase.

Testing equivalence is a powerful means for expressing the security properties of cryptographic protocols, but its formal verification is a difficult task because of the quantification over contexts on which it is based. Previous articles have provided insights into using theorem-proving for the verification of testing equivalence of spi calculus specifications. This article addresses the same verification problem, but uses a state exploration approach. The verification technique is based on the definition of an environment-sensitive, labeled transition system representing a spi calculus specification. Trace equivalence defined on such a transition system coincides with testing equivalence. Symbolic techniques are used to keep the set of traces finite. If a difference in the traces of two spi descriptions (typically a specification and the corresponding implementation of a protocol) is found, it can be used to automatically build the spi calculus description of an intruder process that can exploit the difference.

This paper presents some issues related to the design and implementation of a concurrency analysis tool able to detect deadlock situations in Java programs that make use of multithreading mechanisms. An abstract formal model is generated from the Java source using the Java2Spin translator. The model is expressed in the PROMELA language, and the SPIN tool is used to perform its formal analysis. The paper mainly focuses on the design of the Java2Spin translator. A set of experiments, carried out to evaluate the performances of the analysis tool, is also presented. Copyright © 1999 John Wiley & Sons, Ltd.

The integration of different formal description techniques is an important feature in the design of communication protocols and concurrent systems. In this paper we address the problem of translating Petri nets with inhibitor arcs into basic LOTOS specifications, which is an important step in the direction of integrating these two commonly used formalisms. A mapping which preserves strong bisimulation equivalence is formally defined and illustrated by means of an example. The definition of the mapping enables us also to state a new result about the expressive power of the basic LOTOS subset which constitutes the mapping range.

Performance analysis and formal correctness verification of computer communication protocols and distributed systems have traditionally been considered as two separate fields. However, their integration can be achieved by using formal description techniques as paradigms for the development of performance models. This paper presents a novel extension of LOTOS, one of the two formal specification languages that were standardized by ISO. The extension is specifically conceived to integrate performance analysis and formal verification. The extended language syntax and semantics are formally defined, along with a mapping from extended specifications to performance models, The mapping preserves the specified observable behavior. Two simple examples, a stop-and-wait protocol and a time-sharing system, are used to concretely demonstrate the new approach and to validate it.>

Abstract A new tool for generating implementation prototypes of communication protocols and concurrent systems specified using the ISO LOTOS language is presented in this paper. A brief introduction to LOTOS and a discussion of the main problems related to the efficient execution of specifications written in LOTOS are presented first. The design and implementation of the tool are then considered: LOTOS specifications are analysed and translated into C functions which are executed by co‐operating processes in the Unix environment. The set of LOTOS process definitions is first translated into a suitable number of extended finite‐state machines (EFSMs). The method proposed allows the problem of deriving unbounded EFSMs to be circumvented and a sort of control on the process number/size trade‐off to be obtained at the same time. The problem of implementing the LOTOS multi‐way rendezvous mechanism for process synchronization is solved by using an algorithm based on message‐passing techniques. An example of prototype derivation is also described, showing the form of C code generated by translating a simple specification. Finally, some performance figures are presented.

A generative model for extending algebraic protocol specifications with probabilities is presented. The approach associates a simple probabilistic characterization with each algebraic operator occurrence in a behavior expression. The result is a compact notation in which the assignment of probabilities is more straightforward than with transition-based models. It is shown that an equivalent state machine with probabilities attached to transitions can be constructed automatically from an algebraic specification with probabilistic characterizations attached to operators. Specifically, it is shown how a probabilistic state machine can be derived from a basic LOTOS expression enriched by a probabilistic characterization. As an application example, a stop-and-wait protocol is examined.>

A study of the throughput and time characteristics of double-ring networks is presented, assuming that the two channels are used for balancing the traffic (when both are working) and for synchronous traffic generated according to a generic but periodic pattern. In addition, reconfiguration using portions of both rings to circumvent faulty elements in a double ring network is shown to be equivalent to the single ring configuration already studied. Examples of applications of the results are also illustrated.>

It is noted that the implementation of the multiway rendezvous mechanism of the International Standards Organization (ISO) LOTOS specification language for protocols is very important in the development of tools for the execution of LOTOS. It involves problems such as global knowledge in a distributed environment and distributed agreement. The authors propose a novel algorithm which fully implements the multiway rendezvous of LOTOS within a distributed execution model based on a number of parallel processes. The processes are organized in a hierarchical topology and communicate with each other only by message transfers. The performance of the proposed algorithm is evaluated and is shown to be better than that achieved by other algorithms proposed in the literature. A formal specification of the algorithm in LOTOS is provided.>