Radar systems have long been essential for safe navigation in various transportation sectors, including aviation, maritime, and automotive. While these systems provide invaluable situational awareness and decision-making capabilities, they increasingly become targets for malicious actors aiming to disrupt their normal operations. Electronic countermeasures (ECM) have traditionally been the predominant form of attack. However, recent findings have uncovered their vulnerability to cyber-based actions, capitalizing on their digitization and network connectivity. In this paper, we propose a novel threat model that exploits cyber attack capabilities against radar systems to simulate the effects of ECM. This model goes beyond known attacks by introducing a deceptive element, challenging attribution. To evaluate the feasibility of these attacks, extensive experimentation is conducted using a realistic case study involving the maritime domain. Through this research, we aim to highlight the evolving threats facing radar systems and the need for comprehensive security measures.

The rising of the Cyber-Physical System (CPS) and the Industry 4.0 paradigms demands the design and implementation of Digital Twin Frameworks (DTFs) that may support the quick build of reliable Digital Twins (DTs) for experimental and testing purposes. Most of the current DTF proposals allow the generation of DTs at a good pace but affect generality, scalability, portability, and completeness. As a consequence, current DTF are mostly domain-specific and hardly span several application domains (e.g., from simple IoT deployments to the modeling of complex critical infrastructures). Furthermore, the generated DTs often requires a high amount of computational resource to run. In this paper, we present LiDiTE, a solution based on a novel reference model for general-purpose DTFs. LiDiTE overcomes the limitations of state-of-the-art tools by supporting the fine-grained development of real-world complexity scenarios. To achieve that, LiDiTE builds on technologies that favor scalability, reuse, and extensibility of scenarios. We show such features by building the DT of real critical infrastructure and evaluating the performance of our DT against those of the real system. Further contributions of this paper include open access to the source code of LiDiTE and the experimental dataset.

The operation of radar equipment is one of the key facilities navigators use to gather situational awareness about their surroundings. With an ever-increasing need for always-running logistics and tighter shipping schedules, operators rely more on computerized instruments and their indications. As a result, modern ships have become complex cyber-physical systems in which sensors and computers constantly communicate and coordinate. In this work, we discuss novel threats related to the radar system, one of a ship’s most security-sensitive components. In detail, we first discuss some new attacks capable of compromising the integrity of data displayed on a radar system, with potentially catastrophic impacts on the crew’s situational awareness or safety. Then, we present a detection system to highlight anomalies in the radar video feed, requiring no modifications to the target ship configuration. Finally, we stimulate our detection system by performing the attacks inside a simulated environment. The experimental results indicate that the attacks are feasible, easy to carry out, and hard to detect. Moreover, they prove that the proposed detection technique is effective.

Windows malware detectors based on machine learning are vulnerable to adversarial examples, even if the attacker is only given black-box query access to the model. The main drawback of these attacks is that: ( i) they are query-inefficient, as they rely on iteratively applying random transformations to the input malware; and ( ii) they may also require executing the adversarial malware in a sandbox at each iteration of the optimization process, to ensure that its intrusive functionality is preserved. In this paper, we overcome these issues by presenting a novel family of black-box attacks that are both query-efficient and functionality-preserving, as they rely on the injection of benign content (which will never be executed) either at the end of the malicious file, or within some newly-created sections. Our attacks are formalized as a constrained minimization problem which also enables optimizing the trade-off between the probability of evading detection and the size of the injected payload. We empirically investigate this trade-off on two popular static Windows malware detectors, and show that our black-box attacks can bypass them with only few queries and small payloads, even when they only return the predicted labels. We also evaluate whether our attacks transfer to other commercial antivirus solutions, and surprisingly find that they can evade, on average, more than 12 commercial antivirus engines. We conclude by discussing the limitations of our approach, and its possible future extensions to target malware classifiers based on dynamic analysis.

Recent work has shown that adversarial Windows malware samples—referred to as adversarial EXE mples in this article—can bypass machine learning-based detection relying on static code analysis by perturbing relatively few input bytes. To preserve malicious functionality, previous attacks either add bytes to existing non-functional areas of the file, potentially limiting their effectiveness, or require running computationally demanding validation steps to discard malware variants that do not correctly execute in sandbox environments. In this work, we overcome these limitations by developing a unifying framework that does not only encompass and generalize previous attacks against machine-learning models, but also includes three novel attacks based on practical, functionality-preserving manipulations to the Windows Portable Executable file format. These attacks, named Full DOS , Extend , and Shift , inject the adversarial payload by respectively manipulating the DOS header, extending it, and shifting the content of the first section. Our experimental results show that these attacks outperform existing ones in both white-box and black-box scenarios, achieving a better tradeoff in terms of evasion rate and size of the injected payload, while also enabling evasion of models that have been shown to be robust to previous attacks. To facilitate reproducibility of our findings, we open source our framework and all the corresponding attack implementations as part of the secml-malware Python library. We conclude this work by discussing the limitations of current machine learning-based malware detectors, along with potential mitigation strategies based on embedding domain knowledge coming from subject-matter experts directly into the learning process.

The User Authorization Query (UAQ) Problem is key for RBAC systems that aim to offer permission level user-system interaction, where the system automatically determines the roles to activate in order to enable the requested permissions. Finding a solution to a UAQ problem amounts to determining an optimum set of roles to activate in a given session so to obtain some permissions while satisfying a collection of authorization constraints, most notably Dynamic Mutually-Exclusive Roles (DMER) constraints. Although the UAQ Problem is NP-hard, a number of techniques to solve the UAQ problem have been put forward along with encouraging, albeit inconclusive, experimental results. We propose a methodology for designing parametric benchmarks for the UAQ problem and make a novel suite of parametric benchmarks publicly available that allows for the systematic assessment of UAQ solvers over a number of relevant dimensions. By running three prominent UAQ solvers against our benchmarks, we provide a very comprehensive analysis showing (i) the shortcomings of currently available benchmarks, (ii) the adequacy of the proposed methodology and (iii) that the reduction to PMaxSAT is currently the most effective approach to tackling the UAQ problem.

We present AQUA, a solver for the User Authorization Query (UAQ) problem in Role-Based Access Control (RBAC). The UAQ problem amounts to determining a set of roles granting a given set of permissions, satisfying a collection of authorisation constraints (most notably Dynamic Mutually-Exclusive Roles, DMER) and achieving some optimization objective, i.e. seeking min/max/any number of roles to activate and/or permissions to grant. AQUA supports the enforcement of a wide class of DMER constraints as well as several types of optimization objectives (namely, min/max/any number of roles to activate, min/max/any number of permissions to grant, and a combinations thereof). In this paper, we demonstrate the use of AQUA~over a running example while providing certain implementation details including the architecture.

Cyber Ranges are (virtual) infrastructures for the execution of cyber exercises of the highest quality that simulate cyber scenarios of real-world complexity. Building the computing infrastructure is only the first step towards the successful execution of the cyber exercises. The design, validation, and deployment of scenarios are costly and error-prone activities that may require specialized personnel for weeks or even months. Furthermore, a misconfiguration in the resulting scenario can spoil the entire cyber exercise. In this paper, we propose a framework for automating the (i) design, (ii) model validation, (iii) generation and (iv) testing of cyber scenarios. We introduce a Scenario Definition Language (SDL) based on the OASIS Topology and Orchestration Specification for Cloud Applications (TOSCA). SDL allows for the high level, declarative specification of the components and their interplay. We show that SDL specifications can be encoded into Datalog and that this allows for the automatic checking of the resulting model against a set of validation goals. If the check fails, then a design modification process is triggered. Otherwise, the validated scenario can be automatically deployed on the cyber range. The validation proof is then automatically converted into test cases whose successful execution gives evidence that also the deployed scenario meets the validation goals.

Cross-Site Request Forgery (CSRF) attacks are one of the critical threats to web applications. In this paper, we focus on CSRF attacks targeting web sites' authentication and identity management functionalities. We will refer to them collectively as Authentication CSRF (Auth-CSRF in short). We started by collecting several Auth-CSRF attacks reported in the literature, then analyzed their underlying strategies and identified 7 security testing strategies that can help a manual tester uncover vulnerabilities enabling Auth-CSRF. In order to check the effectiveness of our testing strategies and to estimate the incidence of Auth-CSRF, we conducted an experimental analysis considering 300 web sites belonging to 3 different rank ranges of the Alexa global top 1500. The results of our experiments are alarming: out of the 300 web sites we considered, 133 qualified for conducting our experiments and 90 of these suffered from at least one vulnerability enabling Auth-CSRF (i.e. 68%). We further generalized our testing strategies, enhanced them with the knowledge we acquired during our experiments and implemented them as an extension (namely CSRF-checker) to the open-source penetration testing tool OWASP ZAP. With the help of CSRFchecker, we tested 132 additional web sites (again from the Alexa global top 1500) and identified 95 vulnerable ones (i.e. 72%). Our findings include serious vulnerabilities among the web sites of Microsoft, Google, eBay etc. Finally, we responsibly disclosed our findings to the affected vendors.

While there exist many secure authentication and authorization solutions for web applications, their adaptation in the mobile context is a new and open challenge. In this paper, we argue that the lack of a proper reference model for Single Sign-On (SSO) for mobile native applications drives many social network vendors (acting as Identity Providers) to develop their own mobile solution. However, as the implementation details are not well documented, it is difficult to establish the proper security level of these solutions. We thus provide a rational reconstruction of the Facebook SSO flow, including a comparison with the OAuth 2.0 standard and a security analysis obtained testing the Facebook SSO reconstruction against a set of identified SSO attacks. Based on this analysis, we have modified and generalized the Facebook solution proposing a native SSO solution capable of solving the identified vulnerabilities and accommodating any Identity Provider.

The Android Security Framework controls the executions of applications through permissions which are statically granted by the user during installation. However, the definition of security policies over permissions is not supported. Security policies must be therefore manually encoded into the application by the developer, which is a dangerous practice and may cause security breaches. We propose an improvement over the Android permission system that supports the specification and enforcement of fine-grained security policies. Enforcement is achieved by reducing policy decision problems to propositional satisfiability and leveraging a state-of-the-art SAT solver. Unlike alternative proposals, our approach does not require changes in the operating system and, therefore, it can be readily deployed in any commercial device.

NATO is developing a new IT infrastructure for automated information sharing between different information security domains and supporting dynamic and flexible enforcement of the need-to-know principle. In this context, the Content-based Protection and Release (CPR) model has been introduced to support the specification and enforcement of NATO access control policies. While the ability to define fine-grained security policies for a large variety of users, resources, and devices is desirable, their definition, maintenance, and enforcement can be difficult, time-consuming, and error prone. In this paper, we give an overview of a tool capable of assisting NATO security personnel in these tasks by automatically solving several policy analysis problems of practical interest. The tool levarages state-of-the-art SMT solvers.

The widespread adoption of Application Programming Interfaces (APIs) by enterprises is changing the way business is done by permitting the implementation of a multitude of apps, customized to user needs. While supporting a more flexible exploitation of available data, services and applications developed on top of APIs are vulnerable to a variety of attacks, ranging from SQL injection to unauthorized access of sensitive data. Available security solutions must be re-used and/or adapted to work with APIs. In this paper, we focus on the development of a flexible access control mechanism for APIs. This is an important security mechanism to guarantee the enforcement of authorization constraints on resources while invoking their API functions. We have developed an extension of the Spring Security framework, the standard for securing services and apps built in the popular (open source) Spring framework, for the specification and enforcement of Attribute-Based Access Control (ABAC) policies. We demonstrate our work with scenarios arising in a smart energy eco-system.

Extensions of Role-Based Access Control (RBAC) policies taking into account contextual information (such as time and space) are increasingly being adopted in real-world applications. Their administration is complex since they must satisfy rapidly evolving needs. For this reason, automated techniques to identify unsafe sequences of administrative actions (i.e. actions generating policies by which a user can acquire permissions that may compromise some security goals) are fundamental tools in the administrator's tool-kit. In this paper, we propose a precise and scalable automated analysis technique for the safety of administrative temporal RBAC policies. Our approach is to translate safety problems for this kind of policy to (decidable) reachability problems of a certain class of symbolic transition systems. The correctness of the translation allows us to design a precise analysis technique for the safety of administrative RBAC policies with a finite but unknown number of users. For scalability, we present a heuristics that allows us to reduce the set of administrative actions without losing the precision of the analysis. An extensive experimental analysis confirms the scalability and precision of the approach also in comparison with a recent analysis technique developed for the same class of temporal RBAC policies.

Mobile security is a hot research topic. Yet most of available techniques focus on securing individual applications and therefore cannot possibly tackle security weaknesses stemming from the combined use of one or more applications (e.g. confused deputy attacks). Preventing these types of attacks is crucial in many important application scenarios. For instance, their prevention is a prerequisite for the widespread adoption of the BYOD paradigm in the corporate setting.

The successful operation of NATO missions requires effective and secure sharing of information among coalition partners and external organizations, while avoiding the disclosure of sensitive information to untrusted users. To resolve the conflict between confidentiality and availability, NATO is developing a new information sharing infrastructure, called Content-based Protection and Release. We describe the architecture of access control in NATO operations, which is designed to be easily built on top of available (service-oriented) infrastructures for identity and access control management. We then present a use case scenario drawn from the NATO Passive Missile Defence system for simulating the consequences of intercepting missile attacks. In the system demonstration, we show how maps annotated with the findings of the system are filtered by the access control module to produce appropriate views for users with different clearances and terminals under given release and protection policies.

The User Authorization Query (UAQ) Problem for Role- Based Access Control (RBAC) amounts to determining a set of roles to be activated in a given session in order to achieve some permissions while satisfying a collection of authorization constraints governing the activation of roles. Techniques ranging from greedy algorithms to reduction to (variants of) the propositional satisfiability (SAT) problem have been used to tackle the UAQ problem. Unfortunately, available techniques su er two major limitations that seem to question their practical usability. On the one hand, authorization constraints over multiple sessions or histories are not considered. On the other hand, the experimental evaluations of the various techniques are not satisfactory since they do not seem to scale to larger RBAC policies.

Security contains three papers that originally appeared at the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS '10).The workshop was held on March 27-28, 2010, in Paphos, Cyprus, and affiliated with ETAPS 2010.The workshop brought together researchers interested in developing and applying formal techniques in the development of security-related applications.The three papers in this issue are significant extensions of the workshop papers, and were reviewed according to the normal Journal of Computer Security procedures.The first paper, "Quantitative information flow in interactive systems", by Mário Alvim, Miguel Andrés and Catuscia Palamidessi, considers information flow in a system where secrets and observables alternate during the computation.The authors show that if secrets can depend on the observables, then the system cannot be modelled validly by a classical information-theoretic channel.Instead, they show that this setting corresponds to the notion of channels with memory and feedback.Finally, they show that the channel capacity is a continuous function of a pseudometric based on the Kantorovich metric.The second paper, "Iterative enforcement by suppression: Towards practical enforcement theories", by Nataliia Bielova and Fabio Massacci, considers run-time security enforcement mechanisms.Such mechanisms aim to suppress bad behaviours of a monitored system (i.e., behaviours that do not satisfy the security policy) while not changing good behaviours.The authors observe that when a system does have a bad behaviour, there may be many ways of suppressing it, some of which may be more desirable than others.They define a notion of "better" enforcement, based on the number of elements from the original execution that should be suppressed in order to obtain a legal execution.They then propose a new class of enforcement mechanism, which they show is better than the previously proposed longest-validprefix mechanism.The final paper, "Modular plans for secure service composition", by Gabriele Costa, Pierpaolo Degano and Fabio Martinelli, considers service networks built from open services, i.e. services with unknown components.The authors model services in a variant of the λ-calculus; compliance of a service to a local policy is established by model checking a safe abstraction of the service obtained from a type-and-effect system.The authors describe orchestration plans, which drives the execution at runtime, mapping requests to services.Finally, they define a composition strategy for safely synthesizing a global orchestration plan.

Administrative Role Based Access Control (ARBAC) is one of the most widespread framework for the management of access-control policies. Several automated analysis techniques have been proposed to help maintaining desirable security properties of ARBAC policies. One of the main limitation of availab le analysis techniques is that the set of users is bounded. In this paper, we propose a symbolic framework to overcome this limitation. We design an automated analysis technique that can handle both a bounded and an unbounded number of users by adapting recent methods for the symbolic model checking of infinite state systems that use first-order logic and SMT solving techniques. An extensive experimental evaluation confirms the scalability of the proposed technique.

Automated techniques for the security analysis of Role-Based Access Control (RBAC) access control policies are crucial for their design and maintenance. The definition of administrative domains by means of attributes attached to users makes the RBAC model easier to use in real scenarios but complicates the development of security analysis techniques, that should be able to modularly reason about a wide range of attribute domains. In this paper, we describe an automated symbolic security analysis technique for administrative attribute-based RBAC policies. A class of formulae of first-order logic is used as an adequate symbolic representation for the policies and their administrative actions. State-of-the-art automated theorem proving techniques are used (off-the-shelf) to mechanize the security analysis procedure. Besides discussing the assumptions for the effectiveness and termination of the procedure, we demonstrate its efficiency through an extensive empirical evaluation.

The access to Grid resources depends on rules defined by the administrators of the physical organizations and of the Grid middleware. This approach does not require support for access control in the middleware, but since changes in the access control policy of the Virtual Organization imply the involvement of one or more administrators, it lacks the flexibility needed in a several application scenarios. In this paper we propose a group-based access control model for Grid environments that increases the flexibility of the access control model offered by state-of-the-art Grid platforms without requiring changes in the middleware. The approach is based on collaboration among Grid users and allows them to exchange access permissions to Virtual Resources without the intervention administrators. We show that our solution can be defined on top of the access control mechanisms offered by state-of-the-art Grid middleware and illustrate how the proposed model can be implemented as a service in a service-oriented Grid environment.

Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T . If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems , any theorem-proving strategy with that system and a fair search plan is a T-satisfiability procedure . We prove termination of a rewrite-based first-order engine on the theories of records , integer offsets , integer offsets modulo and lists . We give a modularity theorem stating sufficient conditions for termination on a combination of theories , given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both parametric synthetic benchmarks to test scalability , and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.

Most model checking techniques for security protocols make a number of simplifying assumptions on the protocol and/or on its execution environment that prevent their applicability in some important cases. For instance, most techniques assume that communication between honest principals is controlled by a Dolev -Yao intruder, i.e. a malicious agent capable to overhear, divert, and fake messages. Yet we might be interested in establishing the security of a protocol that relies on a less unsecure channel (e.g. a confidential channel provided by some other protocol sitting lower in the protocol stack). In this paper we propose a general model for security protocols based on the set-rewriting formalism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communication channels as well as complex security properties that are normally not handled by state-of-the-art protocol analysers. By using our approach we have been able to formalise all the assumptions required by the ASW protocol for optimistic fair exchange as well as some of its security properties. Besides the previously reported attacks on the protocol, we report a new attack on a patched version of the protocol.

We describe EUREKA, a symbolic model checker for Linear Programs with arrays, i.e. programs where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. This language fragment easily encodes a large class of programs for which, as demonstrated by our experiments, techniques based on predicate abstraction do not apply successfully.

Maple's evaluator, together with a feature that is usually known as the assume facility, is a combination of modules with specialised resoaning capabilities. These modules are identified, their interfaces are specified, and their interplay is reconstructed as Constraint Contextual Rewriting (CCR), a powerful form of conditional rewriting that incorporates the services provided by a decision procedure. Finally we show how Maple's evaluation process can be strengthened by borrowing ideas from CCR.

We describe a proof plan that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This plan provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This plan makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate the plan with parts of a substantial example-the synthesis of a unification algorithm.

We are mainly interested in the development of CAD systems for interior design. An effective use of such systems relies to a large extent on the characteristics of their user interface. This paper describes NALIG, a system able to "understand" and "reason about" high level descriptions of spatial scenes. The user interacts with the system by using a natural language interface which, though very simple, is expressive enough to allow the description of complex configurations of objects. NALIG replies by drawing on the screen an image mirroring its own "understanding" of the scene described. The comprehension process has required the integration of different AI-techniques (e.g., natural language understanding, spatial reasoning, default and common sense reasoning).

In the last few years, CAD systems have been evolving from simple drafting tools to much more complex solid modeling environments. Nevertheless, experience has shown that effective use of such systems relies on the characteristics of their user interfaces: the user should have the possibility of describing a particular scenario in full detail or giving the system only a raw description of it. The authors describe NALIG, a system able to understand and reason about high-level descriptions of spatial scenes. The user interacts with the system by using a simple natural language fragment that is expressive enough to describe complex configurations of objects. NALIG replies by drawing on the screen an image mirroring its own understanding of the scene that has been described. The comprehension process involves various forms of common-sense reasoning carried out at two different levels of abstraction. This has required the integration of different AI techniques (e.g. natural language understanding, spatial reasoning and default reasoning).