Trusted Execution Environments (TEEs) on resource-constrained microcontrollers are an emerging area of interest, yet they present unique security challenges, particularly in managing encrypted code execution through limited secure memory. This paper presents a formal verification approach for Umbra, a TEE framework for ARM TrustZone-M, currently under development, that implements secure caching mechanisms to execute encrypted enclaves from flash memory. We employ model checking techniques to formally analyze critical security properties, including data isolation between secure and non-secure worlds, integrity of the Enclave Flash Block Cache (EFBC), and resilience against identified threats such as Direct Memory Access (DMA) handover attacks and timing-based side channels. Our threat model considers privileged attackers in the non-secure world and compromised host operating systems, analyzing vulnerabilities in DMA reconfiguration windows and context switch dependencies. Through formal modeling, we identify replay and timing side-channel attacks; by introducing countermeasures, these guarantees are restored in the model.

We study the standard communication problem of broadcast for mobile agents moving in a network, where a single agent called source, has to transmit a vital information to all other agents in the network. The agents move autonomously in the network and can communicate with other agents only when they meet at a node. Previous studies of this problem were restricted to static networks while, in this paper, we consider the problem in dynamic networks modeled as an evolving graph. The dynamicity of the graph is unknown to the agents; in each round an adversary selects which edges of the graph are available, and an agent can choose to traverse one of the available edges adjacent to its current location. The only restriction on the adversary is that the subgraph of available edges in each round must span all nodes; in other words the evolving graph is constantly connected. The agents have global visibility allowing them to see the location of all agents in the graph and move accordingly. Depending on the topology of the underlying graph, we determine the minimum value of k > 0 , such that the broadcast from a source agent to k other agents can be solved in dynamic networks. While k = 2 agents are sufficient for ring networks, much larger teams of agents are necessary for denser graphs such as grid graphs and hypercubes, and finally for complete graphs of n nodes k ≥ n − 2 agents are necessary and sufficient. We show lower bounds on the number of agents and provide algorithms for solving broadcast using the minimum number of agents, for various topologies. These results show how the connectivity of the underlying graph affects the communication capability of a team of mobile agents in constantly connected dynamic networks.

Zero-day malware is a serious cybersecurity concern since it can evade detection techniques using trained and expert systems. In this paper, we propose Z-MDZS - a scheme to effectively identify zero-day malware using a zero-shot1 machine learning approach. Our objective is to detect previously unseen malware based on its properties and relationships to known malware variants, by applying zero-shot learning methods. We evaluate the effectiveness of Z-MDZS, using different machine learning methods, including Random Forest, Deep Neural Networks, and Convolutional Neural Networks. Our results demonstrate that even with smaller feature sets, the zero-shot ML strategy yields solid results, particularly when Random Forest is used as the classifier. Furthermore, we discovered that balancing class samples using Generative Adversarial Network greatly increases classifier accuracy. highlighting its signnificance.

Strand spaces are a formal framework for symbolic protocol verification that allows for pen-and-paper proofs of security [1]. While extremely insightful, pen-and-paper proofs are error-prone, and it is hard to gain confidence on their correctness. To overcome this problem, we developed StrandsRocq, a full mechanization of the strand spaces in Coq (soon to be renamed Rocq). The mechanization was designed to be faithful to the original pen-and-paper development, and it was engineered to be modular and extensible. StrandsRocq incorporates new original proof techniques, a novel notion of maximal penetrator that enables protocol compositionality, and a set of Coq tactics tailored to the domain, facilitating proof automation and reuse, and simplifying the work of protocol analysts. To demonstrate the versatility of our approach, we modelled and analyzed a family of authentication protocols, drawing inspiration from ISO/IEC 9798–2 two-pass authentication, the classical Needham-Schroeder-Lowe protocol, as well as a recently-proposed static analysis for a key management API. The analyses in StrandsRocq confirmed the high degree of proof reuse, and enabled us to distill the minimal requirements for protocol security. Through mechanization, we identified and addressed several issues in the original proofs and we were able to significantly improve the precision of the static analysis for the key management API. Moreover, we were able to leverage the novel notion of maximal penetrator to provide a compositional proof of security for two simple authentication protocols.

Techniques for verifying or invalidating the security of computer systems have come a long way in recent years. Extremely sophisticated tools are available to specify and for-mally verify the behavior of a system and, at the same time, attack techniques have evolved to the point of questioning the possibility of obtaining adequate levels of security, especially in critical applications. In a recent paper, Bognar et al. [1] have clearly highlighted this inconsistency between the two worlds: on one side, formal verification allows writing irrefutable proofs of the security of a system, on the other side concrete attacks make these proofs waver, exhibiting a gap between models and implementations which is very complex to bridge. In this paper, we propose a new method to reduce this gap in the Sancus embedded security architecture, by exploiting some peculiarities of both approaches. Our technique first extracts a behavioral model by directly interacting with the real Sancus system and then analyzes it to identify attacks and anomalies. Given a threat model, our method either finds attacks in the given threat model or gives probabilistic guarantees on the security of the system. We implement our method and use it to systematically rediscover known attacks and uncover new ones.

Time/memory tradeoffs are general techniques used in cryptanalysis that aim at reducing the computational effort in exchange for a higher memory usage. Among these techniques, one of the most modern algorithms is the fuzzy-rainbow tradeoff, which has notably been used in 2010 to attack the GSM A5/1 cipher. Most of the existing analyses of tradeoff algorithms only take into account the main-memory model, which does not reflect the hierarchical (external) storage model of real world systems. Moreover, to the best of our knowledge, there are no publicly available implementations or designs that show the performance level that can be achieved with modern off-the-shelf hardware. In this paper, we propose a reference hardware and software design for the cryptanalysis of ciphers and one-way functions based on FPGAs, SSDs and the fuzzy rainbow tradeoff algorithm. We evaluate the performance of our design by extending an existing analytical model to account for the actual storage hierarchy, and we estimate an attack time for DES and A5/1 ciphers of less than one second, demonstrating that these ciphers can be cracked in real-time with a budget under 6000e.

Hardware Security Modules (HSMs) are trusted machines that perform sensitive operations in critical ecosystems. They are usually required by law in financial and government digital services. The most important feature of an HSM is its ability to store sensitive credentials and cryptographic keys inside a tamper-resistant hardware, so that every operation is done internally through a suitable API, and such sensitive data are never exposed outside the device. HSMs are now conveniently provided in the cloud, meaning that the physical machines are remotely hosted by some provider and customers can access them through a standard API. The property of keeping sensitive data inside the device is even more important in this setting as a vulnerable application might expose the full API to an attacker. Unfortunately, in the last 20+ years a multitude of practical API-level attacks have been found and proved feasible in real devices. The latest version of PKCS#11, the most popular standard API for HSMs, does not address these issues leaving all the flaws possible. In this paper, we propose the first secure HSM configuration that does not require any restriction or modification of the PKCS#11 API and is suitable to cloud HSM solutions, where compliance to the standard API is of paramount importance. The configuration relies on a careful separation of roles among the different HSM users so that known API flaws are not exploitable by any attacker taking control of the application. We prove the correctness of the configuration by providing a formal model in the state-of-the-art Tamarin prover and we show how to implement the configuration in a real cloud HSM solution.

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.

Physical Unclonable Functions (PUFs) are a promising technology to secure low-cost devices. A PUF is a function whose values depend on the physical characteristics of the underlying hardware: the same PUF implemented on two identical integrated circuits will return different values. Thus, a PUF can be used as a unique fingerprint identifying one specific physical device among (apparently) identical copies that run the same firmware on the same hardware. PUFs, however, are tricky to implement, and a number of attacks have been reported in the literature, often due to wrong assumptions about the provided security guarantees and/or the attacker model. In this paper, we present the first mechanized symbolic model for PUFs that allows for precisely reasoning about their security with respect to a variegate set of attackers. We consider mutual authentication protocols based on different kinds of PUFs and model attackers that are able to access PUF values stored on servers, abuse the PUF APIs, model the PUF behavior and exploit error correction data to reproduce the PUF values. We prove security properties and we formally specify the capabilities required by the attacker to break them. Our analysis points out various subtleties, and allows for a systematic comparison between different PUF-based protocols. The mechanized models are easily extensible and can be automatically checked with the Tamarin prover.

We study the standard communication problem of broadcast for mobile agents moving in a network. The agents move autonomously in the network and can communicate with other agents only when they meet at a node. In this model, broadcast is a communication primitive for information transfer from one agent, the source, to all other agents. Previous studies of this problem were restricted to static networks while, in this paper, we consider the problem in dynamic networks modelled as an evolving graph. The dynamicity of the graph is unknown to the agents; in each round an adversary selects which edges of the graph are available, and an agent can choose to traverse one of the available edges adjacent to its current location. The only restriction on the adversary is that the subgraph of available edges in each round must span all nodes; in other words the evolving graph is constantly connected. The agents have global visibility allowing them to see the location of other agents in the graph and move accordingly. Depending on the topology of the underlying graph, we determine how many agents are necessary and sufficient to solve the broadcast problem in dynamic networks. While two agents plus the source are sufficient for ring networks, much larger teams of agents are necessary for denser graphs such as grid graphs and hypercubes, and finally for complete graphs of n nodes at least n-2 agents plus the source are necessary and sufficient. We show lower bounds on the number of agents and provide some algorithms for solving broadcast using the minimum number of agents, for various topologies.

The widespread of smartphones with advanced capabilities has motivated developers to design new mobile applications that are used as barcode scanners. Although several barcode readers are available, they still have security and privacy limitations. In this paper, we first present a comprehensive and systematic review of barcode reader applications by analyzing their security, privacy and usability features. We categorize these apps into four groups depending on their properties: URLs security, Crypto-based security, Popular applications, and Save-privacy. We also highlight their weaknesses and present design recommendations for usable, secure and privacy-guaranteed scanner applications. Based on our recommendations, we have developed BarSec Driod a proof-of-concept secure barcode reader Android app that exploits some features of other applications and at the same time overcomes their limitations. We have performed a user usability and security survey, on BarSec Driod and two other popular QR code readers, KasperSky and QR Droid Private. The results show that BarSec Driod is easy to use, satisfies the expectations of the users and is secure. Moreover, we have observed that following the design tips, user’s security awareness and usability increase.

In complex networks, filters may be applied at different nodes to control how packets flow. In this paper, we study how to locate filtering functionality within a network. We show how to enforce a set of security goals while allowing maximal service subject to the security constraints. To implement our results we present a tool that given a network specification and a set of control rules automatically localizes the filters and generates configurations for all the firewalls in the network. These configurations are implemented using an extension of Mignis - an open source tool to generate firewalls from declarative, semantically explicit configurations. Our contributions include a way to specify security goals for how packets traverse the network, an algorithm to distribute filtering functionality to different nodes in the network to enforce a given set of security goals, and a proof that the results are compatible with a Mignis-based semantics for network behavior.

The management and specification of access control rules that enforce a given policy is a non-trivial, complex, and time consuming task. In this paper we aim at simplifying this task both at specification and verification levels. For that, we propose a formal model of Net filter, a firewall system integrated in the Linux kernel. We define an abstraction of the concepts of chains, rules, and packets existent in Net filter configurations, and give a semantics that mimics packet filtering and address translation. We then introduce a simple but powerful language that permits to specify firewall configurations that are unaffected by the relative ordering of rules, and that does not depend on the underlying Net filter chains. We give a semantics for this language and show that it can be translated into our Net filter abstraction. We then present Mignis, a publicly available tool that translates abstract firewall specifications into real Net filter configurations. Mignis is currently used to configure the whole firewall of the DAIS Department of Ca' Foscari University.

In the past few years, cryptographic key management APIs have been shown to be subject to tricky attacks based on the improper use of cryptographic keys. In fact, real APIs provide mechanisms to declare the intended use of keys but they are not strong enough to provide key security. In this paper, we propose a simple imperative programming language for specifying strongly-typed APIs for the management of symmetric, asymmetric and signing keys. The language requires that type information is stored together with the key but it is independent of the actual low-level implementation. We develop a type-based analysis to prove the preservation of integrity and confidentiality of sensitive keys and we show that our abstraction is expressive enough to code realistic key management APIs.

PKCS#11, is a security API for cryptographic tokens. It is known to be vulnerable to attacks which can directly extract, as cleartext, the value of sensitive keys. In particular, the API does not impose any limitation on the different roles a key can assume, and it permits to perform conflicting op erations such as asking the token to wrap a key with another one and then to decrypt it. Fixes proposed in the literature, or implemented in real devices, impose policies restricting key roles and token functionalities. In this paper we define a simple imperative programming language, suitable to code PKCS#11 symmetric key management, and we develop a type-based analysis to prove that the secrecy of sensitive keys is preserved under a certain policy. We formally analyse existing fixes for PKCS#11 and we propose a new one, which is type-checkable and prevents conflicting roles by deriving different keys for different roles. We develop a prototype type-checker for a software token emulator written in C and we experiment on various working configurations.

Abstract In this article we consider the decontamination problem in a hypercube network of size n. The nodes of the network are assumed to be contaminated and they have to be decontaminated by a sufficient number of agents. An agent is a mobile entity that asynchronously moves along the network links and decontaminates all the nodes it touches. A decontaminated node that is not occupied by an agent is re‐contaminated if it has a contaminated neighbor. We consider some variations of the model based on the capabilities of mobile agents: locality, where the agents can only access local information; visibility, where they can “see” the state of their neighbors; and cloning, where they can create copies of themselves. We also consider synchronicity as an alternative system requirement. For each model, we design a decontamination strategy and we make several observations. For agents with locality, our strategy is based on the use of a coordinator that leads the other agents. Our strategy results in an optimal number of agents, $\Theta ({n \over \sqrt{\log n}})$ , and requires O(n log n) moves and O(n log n) time steps. For agents with visibility, we assume that the agents can move autonomously. In this setting, our decontamination strategy achieves an optimal time complexity (log n time steps), but the number of agents increases to $ {n \over 2}$ . Finally, we show that when the agents have the capability to clone combined with either visibility or synchronicity, we can reduce the move complexity—which becomes optimal—at the expense of an increase in the number of agents. © 2008 Wiley Periodicals, Inc. NETWORKS, 2008

In this paper, we consider the problem of decontaminating a network, i.e., protecting it from unwanted and dangerous intrusions. Initially all nodes are contaminated and a team of agents is deployed to clean the entire network. When an agent transits on a node, it can clean it, when the node is left unguarded, however, it will be recontaminated as soon as at least one of its neighbour is contaminated. We study the problem in asynchronous chordal ring networks with n nodes and chord lengths d/sub 1/ = 1, d/sub 2/, ..., d/sub k/, and in tori. We consider two variations of the model: one where an agent has only local knowledge, the other in which it has "visibility", i.e., it can "see" the state of its neighbouring nodes. We first show that, when the largest chord d/sub k/ is not too large (d/sub k/ /spl les/ /spl radic/n), the number of agents necessary to perform the task in chordal rings does not depend on the size of the network but only on the length of the longest chord. We also show a lower bound on the number of agents for the torus topology. We then propose tight strategies for decontamination. We analyse the number of moves and the time complexity of the decontamination algorithms showing that the visibility assumption allows us to decrease substantially both complexity measures. Another advantage of the "visibility model" is that agents move independently and autonomously without requiring any coordination.

An anonymous ring network is a ring where all processors (vertices) are totally indistinguishable except for their input value. Initially, to each vertex of the ring is associated a value from a totally ordered set; thus, forming a multiset. In this paper we consider the problem of sorting such a distributed multiset and we investigate its relationship with the election problem. We focus on the computability and the complexity of these problems, as well as on their interrelationship, providing strong characterizations, showing lower bounds, and establishing efficient upper bounds.

We consider the problem of routing messages on Series Parallel Graphs (SPGs) and we introduce a new technique called Distance Routing. This technique is based on the idea of encoding in the label of each node x some information about a shortest path from the source of the SPG to x, and from x to the terminal node of the SPG. We first compare shortest path Distance Routing and I-interval Routing Schemes on directed SPGs. We then show that Distance Routing can be used to route on bidirectional SPGs, where no general shortest path I-interval Routing Scheme can be applied. We also show the relevance of the study of the time complexity in the choice of a Compact Routing method.