publications.yml

# PLEASE KEEP ALPHABETICAL ORDER BY ID WITHIN YEARS

## 2010
- id: DISC2010
  id_iris: 21329
  title: "Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - A Case Study"
  authors:
    - FrancescoAlberti
    - SilvioGhilardi
    - ElenaPagani
    - SilvioRanise
    - GianPaoloRossi
  abstract: >
    Background and motivations. Algorithms for ensuring fault tolerance are key ingredients in many applications such as avionics and networking. There is an increasing demand to integrate (formal) validation in the design process of these algorithms as they are often part of safety critical systems.When validation fails, the designer would benefit from tracking the sequence of events that led to an incorrect state to recover the error. To productively integrate formal verification in the design phase, tools should be able to return such error traces. Fault tolerant algorithms are often parametric, which makes their automated verification a daunting task. Indeed, checking that an algorithm satisfies a certain property requires to prove it for any number of processes.
  destination: DISC2010
  year: 2010
  doi: 10.1007/978-3-642-15763-9_36

- id: HVC2010
  id_iris: 21635
  title: Automated Symbolic Analysis of ARBAC Policies
  authors:
    - ClarkBarrett
    - LeonardoDeMoura
    - SilvioRanise
    - AaronStump
    - CesareTinelli
  abstract: >
    Satisfiability modulo theories (SMT) is a branch of automated reasoning that builds on advances in propositional satisfiability and on decision procedures for first-order reasoning. Its defining feature is the use of reasoning methods specific to logical theories of interest in target applications. Advances in SMT research and technology have led in the last few years to the development of very powerful satisfiability solvers and to an explosion of applications. SMT solvers are now used for processor verification, equivalence checking, bounded and unbounded model checking, predicate abstraction, static analysis, automated test case generation, extended static checking, scheduling and optimization. While the roots of SMT go back to work in the late 1970s and early 1980s on using decision procedures in formal methods, the field was born in the late 1990s with various independent attempts to harness the power of modern SAT solvers, reaching the current level of sophistication with the research and development advances of the last decade. Major enablers for these advances were SMT-LIB, a standardization and benchmark collection initiative supported by a large number of SMT researchers and users world-wide, and its offsprings: the SMT workshop, an international workshop bringing together SMT researchers and users of SMT applications or techniques; SMT-COMP, an international competition for SMT solvers supporting the SMT-LIB input format; and SMT-EXEC, a public execution service allowing researchers to configure and execute benchmarking experiments on SMT solvers.
    This talk provides historical perspectives on the development of the field and on the SMT-LIB initiative and its offsprings. It highlights the initiative’s milestones and main achievements, and the role of the authors and other major contributors in it. It then concludes with a brief discussion of a few promising directions for future research in SMT.
  destination: HVC2010
  year: 2010
  doi: 10.1007/978-3-642-19583-9_2

- id: IJCAR2010
  id_iris: 21309
  title: "MCMT: A Model Checker Modulo Theories"
  authors:
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    We describe mcmt, a fully declarative and deductive symbolic model checker for safety properties of infinite state systems whose state variables are arrays. Theories specify the properties of the indexes and the elements of the arrays. Sets of states and transitions of a system are described by quantified first-order formulae. The core of the system is a backward reachability procedure which symbolically computes pre-images of the set of unsafe states and checks for safety and fix-points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics for quantifier instantiation, specifically tailored to model checking, are at the very heart of the system. mcmt has been successfully applied to the verification of imperative programs, parametrised, timed, and distributed systems.
  destination: IJCAR2010
  year: 2010
  doi: 10.1007/978-3-642-14203-1_3

- id: LMCS2010
  id_iris: 50380
  title: "Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis"
  authors:
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    The safety of infinite state systems can be checked by a backward reachability procedure. For certain classes of systems, it is possible to prove the termination of the procedure and hence conclude the decidability of the safety problem. Although backward reachability is property-directed, it can unnecessarily explore (large) portions of the state space of a system which are not required to verify the safety property under consideration. To avoid this, invariants can be used to dramatically prune the search space. Indeed, the problem is to guess such appropriate invariants. In this paper, we present a fully declarative and symbolic approach to the mechanization of backward reachability of infinite state systems manipulating arrays by Satisfiability Modulo Theories solving. Theories are used to specify the topology and the data manipulated by the system. We identify sufficient conditions on the theories to ensure the termination of backward reachability and we show the completeness of a method for invariant synthesis (obtained as the dual of backward reachability), again, under suitable hypotheses on the theories. We also present a pragmatic approach to interleave invariant synthesis and backward reachability so that a fix-point for the set of backward reachable states is more easily obtained. Finally, we discuss heuristics that allow us to derive an implementation of the techniques in the model checker MCMT, showing remarkable speed-ups on a significant set of safety problems extracted from a variety of sources.
  destination: LMCS
  year: 2010
  doi: 10.2168/LMCS-6(4:10)2010

- id: STM2010
  id_iris: 21635
  title: Automated Symbolic Analysis of ARBAC Policies
  authors:
    - AlessandroArmando
    - SilvioRanise
  abstract: >
    One of the most widespread framework for the management of access-control policies is Administrative Role Based Access Control (ARBAC). Several automated analysis techniques have been proposed to help maintaining desirable security properties of ARBAC policies. One limitation of many available techniques is that the sets of users and roles are bounded. In this paper, we propose a symbolic framework to overcome this difficulty. We design an automated security analysis technique, parametric in the number of users and roles, by adapting recent methods for model checking infinite state systems that use first-order logic and state-of-the-art theorem proving techniques. Preliminary experiments with a prototype implementations seem to confirm the scalability of our technique.
  destination: STM2010
  year: 2010
  doi: 10.1007/978-3-642-22444-7_2

- id: SYNASC2010
  id_iris: 50391
  title: "WSSMT: Towards the Automated Analysis of Security-Sensitive Services and Applications"
  authors:
    - MicheleBarletta
    - AlbertoCalvi
    - SilvioRanise
    - LucaViganò
    - LucaZanetti
  abstract: >
    The security of service-oriented applications is crucial in several contexts such as e-commerce or e-governance. The design, implementation, and deployment of this kind of services are often so complex that serious vulnerabilities remain even after extensive application of traditional validation techniques, such as testing. Given the importance of security-sensitive service applications, the development of techniques for their automated validation is growing. In this paper, we illustrate our formal framework to the specification and validation of security-sensitive applications structured in two levels: the workflow level (dealing with the control of flow and the manipulation of data) and the policy level (describing trust relationships and access control). In our framework, verification problems are reduced to logical problems whose decidability can be shown under suitable assumptions, which permit the validation of practically relevant classes of services. As a by-product, it is possible to re-use state-of-the-art theorem-proving technology to mechanize the verification process. This is the idea underlying our prototype validation tool WSSMT, "Web-Service (validation by) Satisfiability Modulo Theories'', which has been successfully used on two industrial case studies taken from the FP7 European project AVANTSSAR.
  destination: SYNASC2010
  year: 2010
  doi: 10.1109/SYNASC.2010.74

- id: SYNASC2010_Validation
  id_iris: 50392
  title: Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC
  authors:
    - AlbertoCalvi
    - SilvioRanise
    - LucaViganò
  abstract: >
    We formalize automated analysis techniques for the validation of web services specified in BPEL and a RBAC variant tailored to BPEL. The idea is to use decidable fragments of first-order logic to describe the state space of a certain class of web services and then use state-of-the-art SMT solvers to handle their reach ability problems. To assess the practical viability of our approach, we have developed a prototype tool implementing our techniques and applied it to a digital contract signing service inspired by an industrial case study.
  destination: SYNASC2010
  year: 2010
  doi: 10.1109/SYNASC.2010.75

## 2011
- id: ASIACCS2011
  id_iris: 21617
  title: Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-Policies
  authors:
    - FrancescoAlberti
    - AlessandroArmando
    - SilvioRanise
  abstract: >
    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.
  destination: ASIACCS2011
  year: 2011
  doi: 10.1145/1966913.1966935

- id: CADE2011
  id_iris: 50384
  title: "ASASP: Automated Symbolic Analysis of Security Policies"
  authors:
    - FrancescoAlberti
    - AlessandroArmando
    - SilvioRanise
  abstract: >
    We describe asasp, a symbolic reachability procedure for the analysis of administrative access control policies. The tool represents access policies and their administrative actions as formulae of the Bernays-Shönfinkel-Ramsey class and then uses a symbolic reachability procedure to solve security analysis problems. Checks for fix-point—reduced to satisfiability problems—are mechanized by Satisfiability Modulo Theories solving and Automated Theorem Proving. asasp has been successfully applied to the analysis of benchmark problems arising in (extensions of) the Role-Based Access Control model. Our tool shows better scalability than a state-of-the-art tool on a significant set of instances of these problems.
  destination: CADE2011
  year: 2011
  doi: 10.1007/978-3-642-22438-6_4

- id: FroCoS2011
  id_iris: 50387
  title: A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints
  authors:
    - RobertoBruttomesso
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    The use of interpolants in model checking is progressively gaining importance. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general. To overcome this problem, we have recently proposed a quantifier-free interpolation solver for a natural variant of the theory of arrays. However, arrays are usually combined with fragments of arithmetic over indexes in applications, especially those related to software verification. In this paper, we propose a quantifier-free interpolation solver for the variant of arrays considered in previous work when combined with integer difference logic over indexes.
  destination: FroCoS2011
  year: 2011
  doi: 10.1007/978-3-642-24364-6_8

- id: IC2011
  id_iris: 50382
  title: Automatic Decidability and Combinability
  authors:
    - ChristopherLynch
    - SilvioRanise
    - ChristopheRingeissen
    - DucKhahnTran
  abstract: >
    Verification problems can often be encoded as first-order validity or satisfiability problems. The availability of efficient automated theorem provers is a crucial pre-requisite for automating various verification tasks as well as their cooperation with specialized decision procedures for selected theories, such as Presburger Arithmetic. In this paper, we investigate how automated provers based on a form of equational reasoning, called paramodulation, can be used in verification tools. More precisely, given a theory T axiomatizing some data structure, we devise a procedure to answer the following questions. Is the satisfiability problem of T decidable by paramodulation? Can a procedure based on paramodulation for T be efficiently combined with other specialized procedures by using the Nelson–Oppen schema? Finally, if paramodulation decides the satisfiability problem of two theories, does it decide satisfiability in their union?
    The procedure capable of answering all questions above is based on Schematic Saturation; an inference system capable of over-approximating the inferences of paramodulation when solving satisfiability problems in a given theory T. Clause schemas derived by Schematic Saturation describe all clauses derived by paramodulation so that the answers to the questions above are obtained by checking that only finitely many different clause schemas are derived or that certain clause schemas are not derived.
  destination: IC
  destinationAddon: Volume 209, Issue 7, July 2011, Pages 1026-1047
  year: 2011
  doi: 10.1016/j.ic.2011.03.005

- id: ICSC2011
  id_iris: 50388
  title: "Automated analysis of semantic-aware access control policies: a logic-based approach"
  authors:
    - AlessandroArmando
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    As the number and sophistication of on-line applications increase, there is a growing concern on how access to sensitive resources (e.g., personal health records) is regulated. Since ontologies can support the definition of fine-grained policies as well as the combination of heterogeneous policies, semantic technologies are expected to play an important role in this context. But understanding the implications of the access control policies of the needed complexity goes beyond the ability of a security administrator. Automatic support to the analysis of access control policies is therefore needed. In this paper we present an automatic analysis technique for access control policies that reduces the reach ability problem for access control policies to satisfiability problems in a decidable fragment of first-order logic for which efficient solvers exist. We illustrate the application of our technique on an access control model inspired by a Personal Health Application of real-world complexity.
  destination: ICSC2011
  year: 2011
  doi: 10.1109/ICSC.2011.74

- id: RP2011
  id_iris: 50386
  title: Automated Termination in Model Checking Modulo Theories
  authors:
    - AlessandroCarioni
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    We use a declarative SMT-based approach to model-checking of infinite state systems to design a procedure for automatically establishing the termination of backward reachability by using well-quasi-orderings. Besides showing that our procedure succeeds in many instances of problems covered by general termination results, we argue that it could predict termination also on single problems outside the scope of applicability of such general results.
  destination: RP2011
  year: 2011
  doi: 10.1007/978-3-642-24288-5_11

- id: RTA2011
  id_iris: 50383
  title: Rewriting-based Quantifier-free Interpolation for a Theory of Arrays
  authors:
    - RobertoBruttomesso
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general. In this paper, we show that, with a minor extension to the theory of arrays, it is possible to obtain quantifier-free interpolants. We prove this by designing an interpolating procedure, based on solving equations between array updates. Rewriting techniques are used in the key steps of the solver and its proof of correctness. To the best of our knowledge, this is the first successful attempt of computing quantifier-free interpolants for a theory of arrays.
  destination: RTA2011
  year: 2011
  doi: 10.4230/LIPIcs.RTA.2011.171

- id: SCPE2011
  id_iris: 50390
  title: "Workflow and Access Control Reloaded: a Declarative Specification Framework for the Automated Analysis of Web Services"
  authors:
    - MicheleBarletta
    - AlbertoCalvi
    - SilvioRanise
    - LucaViganò
    - LucaZanetti
  abstract: >
    Web services supporting business and administrative transactions between several parties over the Internet are more and more widespread. Their development involves several security issues ranging from authentication to the management of the access to shared resources according to given business and legal models. The capability of validating designs against fast evolving requirements is of paramount importance for the adaptation of business and administrative models to changing regulations and rapidly evolving market needs. We present formal specification and analysis techniques that allow us to validate the designs of security-sensitive web services specified in the Business Process Execution Language and extensions of the Role-Based Access Control model. We also present a prototype tool, called \WSSMT{}, mechanizing our approach and describe our experience in using it on two industrial case studies, on in the e-business and one in the e-government area.
  destination: SCPE
  year: 2011
  doi: 10.1007/s11761-010-0073-4

- id: SOCA2011
  id_iris: 50381
  title: A declarative two-level framework to specify and verify workflow and authorization policies in service-oriented architectures
  authors:
    - MicheleBarletta
    - SilvioRanise
    - LucaViganò
  abstract: >
    The specification of distributed service-oriented applications spans several levels of abstraction, e.g., the protocol for exchanging messages, the set of interface functionalities, the types of the manipulated data, the workflow, the access policy, etc. Many (even executable) specification languages are available to describe each level in separation. However, these levels may interact in subtle ways (for example, the control flow may depend on the values of some data variables) so that a precise abstraction of the application amounts to more than the sum of its per level components. This problem is even more acute in the design phase when automated analysis techniques may greatly help the difficult task of building “correct” applications faced by designers. To alleviate this kind of problems, this paper introduces a framework for the formal specification and automated analysis of distributed service-oriented applications in two levels: one for the workflow and one for the authorization policies. The former allows one to precisely describe the control and data parts of an application with their mutual dependencies. The latter focuses on the specification of the criteria for granting or denying third-party applications the possibility to access shared resources or to execute certain interface functionalities. These levels can be seen as abstractions of one or of several levels of specification mentioned above. The novelty of our proposal is the possibility to unambiguously specify the—often subtle—interplay between the workflow and policy levels uniformly in the same framework. Additionally, our framework allows us to define and investigate verification problems for service-oriented applications (such as executability and invariant checking) and give sufficient conditions for their decidability. These results are non-trivial because their scope of applicability goes well beyond the case of finite state spaces allowing for applications manipulating variables ranging over infinite domains. As proof of concept, we show the suitability and flexibility of our approach on two quite different examples inspired by industrial case studies.
  destination: SOCA
  year: 2011
  doi: 10.1007/s11761-010-0073-4

- id: STM2011
  id_iris: 50385
  title: Automated Analysis of Infinite State Workflows with Access Control Policies
  authors:
    - AlessandroArmando
    - SilvioRanise
  abstract: >
    Business processes are usually specified by workflows extended with access control policies. In previous works, automated techniques have been developed for the analysis of authorization constraints of workflows. One of main drawback of available approaches is that only a bounded number of workflow instances is considered and analyses are limited to consider intra-instance authorization constraints. Instead, in applications, several workflow instances execute concurrently, may synchronize, and be required to ensure inter-instance constraints. Performing an analysis by considering a finite but arbitrary number of workflow instances can give designers a higher confidence about the quality of their business process. In this paper, we propose an automated technique for the analysis of both intra- and inter-instance authorization constraints in workflow systems. We reduce the analysis problem to a model checking problem, parametric in the number of workflow instances, and identify a sub-class of workflow systems with a decidable analysis problem.
  destination: STM2011
  year: 2011
  doi: 10.1007/978-3-642-29963-6_12

## 2012
- id: CAV2012
  id_iris: 101402
  title: "SAFARI: SMT-Based Abstraction for Arrays with Interpolants"
  authors:
    - FrancescoAlberti
    - RobertoBruttomesso
    - SilvioGhilardi
    - SilvioRanise
    - NatashaSharygina
  abstract: >
    We present SAFARI, a model checker designed to prove (possibly universally quantified) safety properties of imperative programs with arrays of unknown length. SAFARI is based on an extension of lazy abstraction capable of handling existentially quantified formulæ for symbolically representing states. A heuristics, called term abstraction, favors the convergence of the tool by “tuning” interpolants and guessing additional quantified variables of invariants to prune the search space efficiently.
  destination: CAV2012
  year: 2012
  doi: 10.1007/978-3-642-31424-7_49

- id: CODASPY2012
  id_iris: 101401
  title: "Efficient run-time solving of RBAC user authorization queries: pushing the envelope"
  authors:
    - AlessandroArmando
    - SilvioRanise
    - FatihTurkmen
    - BrunoCrispo
  abstract: >
    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.
    In this paper, we describe a SAT-based technique to solve the UAQ problem which overcomes these limitations. First, we show how authorization constraints over multiple sessions and histories can be supported. Second, we carefully tune the reduction to the SAT problem so that most of the clauses need not to be generated at run-time but only in a pre-processing step. Finally, we present an extensive experimental evaluation of an implementation of our techniques on a significant set of UAQ problem instances that show the practical viability of our approach; e.g., problems with 300 roles are solved in less than a second.
  destination: CODASPY2012
  year: 2012
  doi: 10.1145/2133601.2133631

- id: DBSec2012
  id_iris: 101206
  title: Automated and Efficient Analysis of Role-Based Access Control with Attributes
  authors:
    - AlessandroArmando
    - SilvioRanise
  abstract: >
    We consider an extension of the Role-Based Access Control model in which rules assign users to roles based on attributes. We consider an open (allow-by-default) policy approach in which rules can assign users negated roles thus preventing access to the permissions associated to the role. The problems of detecting redundancies and inconsistencies are formally stated. By expressing the conditions on the attributes in the rules with formulae of theories that can be efficiently decided by Satisfiability Modulo Theories (SMT) solvers, we characterize the decidability and complexity of the problems of detecting redundancies and inconsistencies. The proof of the result is constructive and based on an algorithm that repeatedly solves SMT problems. An experimental evaluation with synthetic benchmark problems shows the practical viability of our technique.
  destination: DBSec2012
  year: 2012
  doi: 10.1007/978-3-642-31540-4_3

- id: IJCAR2012
  id_iris: 101205
  title: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
  authors:
    - RobertoBruttomesso
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the ‘strong (sub-)amalgamation’ property. Then, we provide an equivalent syntactic characterization, identify a sufficient condition, and design a combined quantifier-free interpolation algorithm handling both convex and non-convex theories, that subsumes and extends most existing work on combined interpolation.
  destination: IJCAR2012
  year: 2012
  doi: 10.1007/978-3-642-31365-3_12

- id: JCS2012
  id_iris: 121401
  title: Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving
  authors:
    - AlessandroArmando
    - SilvioRanise
  abstract: >
    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 available 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.
  destination: JCS
  destinationAddon: vol. 20, no. 4, pp. 309-352
  year: 2012
  doi: 10.3233/JCS-2012-0461

- id: JSAT2012
  id_iris: 101202
  title: Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories
  authors:
    - FrancescoAlberti
    - SilvioGhilardi
    - ElenaPagani
    - SilvioRanise
    - GianPaoloRossi
  abstract: >
    Model Checking Modulo Theories is a recent approach for the automated verification of safety properties of a class of infinite state systems manipulating arrays, called array-based systems. The idea is to repeatedly compute pre-images of a set of (unsafe) states by using certain classes of first-order formulae representing sets of states and transitions, and then reduce fix-point checks to Satisfiability Modulo Theories problems. Unfortunately, if the guards contain universally quantified index variables, the backward procedure cannot be fully automated. In this paper, we overcome the problem by describing a syntactic transformation on array-based systems, which can be seen as an instance of the well-known operation of relativization of quantifiers in first-order logic. Interestingly, when specifying and verifying distributed systems, the proposed syntactic transformation can be interpreted as the adoption of the crash-failure model, which is well-known in the literature of fault-tolerant systems. By eliminating universal quantifiers from guards, the transformation significantly extends the scope of applicability of the symbolic backward reachability procedure. To provide empirical evidence of this claim, we discuss our findings in applying the proposed technique to a significant case-study in the verification of some classical algorithms for reliable broadcast.
  destination: JSAT
  year: 2012
  doi: 10.3233/SAT190087

- id: JSC2012
  id_iris: 50389
  title: On the Verification of Security-Aware E-services
  authors:
    - SilvioRanise
  abstract: >
    Web services providing E-commerce capabilities to support business transactions over the Internet are more and more widespread. The development of such services involves several security issues ranging from authentication to the management of the access to shared resources according to a given business model. The capability of validating designs against fast evolving requirements is of paramount importance for the adaptation of business models to changing regulations and rapidly evolving market needs. So, techniques for the specification and automated analysis of web services to be used in security-sensitive applications are crucial in the development of these systems.
    In this paper, we propose an extension of the relational transducers introduced by Abiteboul, Vianu, Fordham, and Yesha for the specification of the transaction protocols of web services and their security properties. We investigate the decidability of relevant verification problems such as goal reachability (for the validation of use-case scenarios) and log validation (for detecting frauds) and provide sufficient conditions for their decidability. The extension we propose is two-fold. First, we add constraints to specify the algebraic structure of the resources manipulated by the transducers. Second, recursion is allowed (only) in policy rules to express important policy idioms such as delegation. Technically, decidability is obtained by a reduction to a decidable class of first-order formulae and fix-point computation to handle recursion.
  destination: JSC
  destinationAddon: Volume 47, Issue 9
  year: 2012
  doi: 10.1016/j.jsc.2011.12.033

- id: LMCS2012
  id_iris: 101201
  title: Quantifier-Free Interpolation of a Theory of Arrays
  authors:
    - RobertoBruttomesso
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier- free interpolants in general. In this paper, we show that it is possible to obtain quantifier-free interpolants for a Skolemized version of the extensional theory of arrays. We prove this in two ways: (1) non-constructively, by using the model theoretic notion of amalgamation, which is known to be equivalent to admit quantifier-free interpolation for universal theories; and (2) constructively, by designing an interpolating procedure, based on solving equations between array updates. (Interestingly, rewriting techniques are used in the key steps of the solver and its proof of correctness.) To the best of our knowledge, this is the first successful attempt of computing quantifier- free interpolants for a variant of the theory of arrays with extensionality. 
  destination: LMCS
  destinationAddon: Volume 8, Issue 2
  year: 2012
  doi: 10.2168/LMCS-8(2:4)2012

- id: LPAR2012
  id_iris: 101204
  title: Lazy Abstraction with Interpolants for Arrays
  authors:
    - FrancescoAlberti
    - RobertoBruttomesso
    - SilvioGhilardi
    - SilvioRanise
    - NatashaSharygina
  abstract: >
    Lazy abstraction with interpolants has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method shows an intrinsic limitation, due to the fact that successful invariants usually contain universally quantified variables, which are not present in the program specification. In this work we present an extension of the interpolation-based lazy abstraction in which arrays of unknown length can be handled in a natural manner. In particular, we exploit the Model Checking Modulo Theories framework, to derive a backward reachability version of lazy abstraction that embeds array reasoning. The approach is generic, in that it is valid for both parameterized systems and imperative programs. We show by means of experiments that our approach can synthesize and prove universally quantified properties over arrays in a completely automatic fashion.
  destination: LPAR
  year: 2012
  doi: 10.1007/978-3-642-28717-6_7

- id: NFM2012
  id_iris: 101203
  title: Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms
  authors:
    - RobertoBruttomesso
    - AlessandroCarioni
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    Deadlock-free algorithms that ensure mutual exclusion crucially depend on timing assumptions. In this paper, we describe our experience in automatically verifying mutual-exclusion and deadlock-freedom of the Fischer and Lynch-Shavit algorithms, using the model checker modulo theories mcmt. First, we explain how to specify timing-based algorithms in the mcmt input language as symbolic transition systems. Then, we show how the tool can verify all the safety properties used by Lynch and Shavit to establish mutual-exclusion, regardless of the number of processes in the system. Finally, we verify deadlock-freedom by following a reduction to “safety problems with lemmata synthesis” and using acceleration to avoid divergence. We also show how to automatically synthesize the bounds on the waiting time of a process to enter the critical section.
  destination: NFM2012
  year: 2012
  doi: 10.1007/978-3-642-28891-3_28

- id: NSS2012
  id_iris: 101403
  title: "On the Automated Analysis of Safety in Usage Control: A New Decidability Result"
  authors:
    - SilvioRanise
    - AlessandroArmando
  abstract: >
    We study the decidability of the safety problem in the usage control (UCON) model. After defining a formal model, we identify sufficient conditions for the decidability of the safety problem for UCON systems whose attributes are allowed to range over infinite domains and updates in one process may affect the state of another. Our result is a significant generalization of those available in the literature.
  destination: NSS2012
  year: 2012
  doi: 10.1007/978-3-642-34601-9_2

- id: STM2012
  id_iris: 101602
  title: Boosting Model Checking to Analyse Large ARBAC Policies
  authors:
    - SilvioRanise
    - TuanAnhTruong
    - AlessandroArmando
  abstract: >
    The administration of access control policies is a task of paramount importance for distributed systems. A crucial analysis problem is to foresee if a set of administrators can give a user an access permission. We consider this analysis problem in the context of the Administrative Role-Based Access Control (ARBAC), one of the most widespread administrative models. Given the difficulty of taking into account the effect of all possible administrative actions, automated analysis techniques are needed. In this paper, we describe how a model checker can scale up to handle very large ARBAC policies while ensuring completeness. An extensive experimentation shows that an implementation of our techniques performs significantly better than Mohawk, a recently proposed tool that has become the reference for finding errors in ARBAC policies.
  destination: STM2012
  year: 2012
  doi: 10.1007/978-3-642-38004-4_18

- id: STM2012_DAC
  id_iris: 101601
  title: Automated Analysis of Scenario-based Specifications of Distributed Access Control Policies with Non-Mechanizable Activities
  authors:
    - MicheleBarletta
    - SilvioRanise
    - LucaViganò
  abstract: >
    The advance of web services technologies promises to have far-reaching effects on the Internet and enterprise networks allowing for greater accessibility of data. The security challenges presented by the web services approach are formidable. In particular, access control solutions should be revised to address new challenges, such as the need of using certificates for the identification of users and their attributes, human intervention in the creation or selection of the certificates, and (chains of) certificates for trust management. With all these features, it is not surprising that analyzing policies to guarantee that a sensitive resource can be accessed only by authorized users becomes very difficult. In this paper, we present an automated technique to analyze scenario-based specifications of access control policies in open and distributed systems. We illustrate our ideas on a case study arising in the e-government area.
  destination: STM2012
  year: 2012
  doi: 10.1007/978-3-642-38004-4_4

## 2013
- id: FMSD2013
  id_iris: 180610
  title: Symbolic backward reachability with effectively propositional logic
  authors:
    - SilvioRanise
  abstract: >
    We describe a symbolic procedure for solving the reachability problem of transition systems that use formulae of Effectively Propositional Logic to represent sets of backward reachable states. We discuss the key ideas for the mechanization of the procedure where fix-point checks are reduced to SMT problems. We also show the termination of the procedure on a sub-class of transition systems. Then, we discuss how reachability problems for this sub-class can be used to encode analysis problems of administrative policies in the Role-Based Access Control (RBAC) model that is one of the most widely adopted access control paradigms. An implementation of a refinement of the backward reachability procedure, called asasp, shows better flexibility and scalability than a state-of-the-art tool on a significant set of security problems.
  destination: FMSD
  year: 2013
  doi: 10.1007/s10703-012-0157-1

- id: FroCoS2013
  id_iris: 180614
  title: Verification of Composed Array-based Systems with Applications to Security-Aware Workflows
  authors:
    - ClaraBertolissi
    - SilvioRanise
  abstract: >
    We introduce a class of symbolic transition systems capable of representing collections of security-aware workflows and we study the verification of reachability properties of such systems. More precisely, we define composed array-based systems as an extension of array-based systems in which array variables are indexed over more than one type. For an application relevant sub-class of these systems we show how to mechanize a symbolic backward reachability procedure by modularly re-using the techniques developed for array-based systems. Finally, and most importantly, we find sufficient conditions for the termination of the procedure and we apply this result to derive the decidability of the reachability problems of two important classes of security-aware workflow systems.
  destination: FroCoS2013
  year: 2013
  doi: 10.1007/978-3-642-40885-4_4
  urlNews: /news/2013/06/06/paper-accepted-at-frocos-2013/

- id: FPS2013
  id_iris: 226615
  title: Formal Modelling of Content-Based Protection and Release for Access Control in NATO Operations
  authors:
    - AlessandroArmando
    - SanderOudkerk
    - SilvioRanise
    - KonradWrona
  abstract: >
    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.
  destination: FPS2013
  year: 2013
  doi: 10.1007/978-3-319-05302-8_14
  urlNews: /news/2013/08/27/paper-accepted-at-fps2013/

- id: ICITST2013
  id_iris: 222616
  title: A methodology to build run-time monitors for security-aware workflows
  authors:
    - ClaraBertolissi
    - SilvioRanise
  abstract: >
    Run-time monitors are crucial to the development of workflow management systems, which are at the heart of several modern E-services. In this paper, we propose a new methodology to build run-time monitors capable of ensuring the successful termination of workflows subject to authorization constraints. The methodology is based on state-of-the-art Satisfiability Modulo Theories techniques.
  destination: ICITST2013
  year: 2013
  doi: 10.1109/ICITST.2013.6750251

- id: IJFCS2013
  id_iris: 180611
  title: Automated Termination in Model-Checking Modulo Theories
  authors:
    - AlessandroCarioni
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic.
  destination: IJFCS
  year: 2013
  doi: 10.1142/S012905411340008X

- id: SACMAT2013
  id_iris: 180613
  title: Content-based information protection and release in NATO operations
  authors:
    - AlessandroArmando
    - MatteoGrasso
    - SanderOudkerk
    - SilvioRanise
    - KonradWrona
  abstract: >
    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.
  destination: SACMAT2013
  year: 2013
  doi: 10.1145/2462410.2462427

## 2014
- id: CSET2014
  id_iris: 250446
  title: "TESTREX: a Testbed for Repeatable Exploits"
  authors:
    - StanislavDashevskyi
    - DanielDosSantos
    - FabioMassacci
    - AntoninoSabetta
  destination: CSET2014
  year: 2014
  urlNews: /news/2014/06/09/paper-accepted-at-cset14/

- id: DBSec2014
  id_iris: 226015
  title: "Incremental Analysis of Evolving Administrative Role Based Access Control Policies"
  authors:
    - SilvioRanise
    - TuanAnhTruong
  abstract: >
    We consider the safety problem for Administrative Role-Based Access Control (ARBAC) policies, i.e. detecting whether sequences of administrative actions can result in policies by which a user can acquire permissions that may compromise some security goals. In particular, we are interested in sequences of safety problems generated by modifications (namely, adding/deleting an element to/from the set of possible actions) to an ARBAC policy accommodating the evolving needs of an organization. or resulting from fixing some safety issues. Since problems in such sequences share almost all administrative actions, we propose an incremental technique that avoids the re-computation of the solution to the current problem by re-using much of the work done on the previous problem in a sequence. An experimental evaluation shows the better performances of an implementation of our technique with respect to the only available approach to solve safety problems for evolving ARBAC policies proposed by Gofman, Luo, and Yang.
  destination: DBSec2014
  year: 2014
  doi: 10.1007/978-3-662-43936-4_17

- id: FMSD2014
  id_iris: 269019
  title: An extension of lazy abstraction with interpolation for programs with arrays
  authors:
    - FrancescoAlberti
    - RobertoBruttomesso
    - SilvioGhilardi
    - SilvioRanise
    - NatashaSharygina
  abstract: >
    Lazy abstraction with interpolation-based refinement has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method suffers from an intrinsic limitation, due to the fact that invariants needed for verification usually contain universally quantified variables, which are not present in program specifications. In this work we present an extension of the interpolation-based lazy abstraction framework in which arrays of unknown length can be handled in a natural manner. In particular, we exploit the Model Checking Modulo Theories framework to derive a backward reachability version of lazy abstraction that supports reasoning about arrays. The new approach has been implemented in a tool, called safari, which has been validated on a wide range of benchmarks. We show by means of experiments that our approach can synthesize and prove universally quantified properties over arrays in a completely automatic fashion.
  destination: FMSD
  year: 2014
  doi: 10.1007/s10703-014-0209-9

- id: NOMS2014
  id_iris: 250444
  title: A Dynamic Risk-based Access Control Architecture for Cloud Computing
  authors:
    - DanielDosSantos
    - CarlaMerkleWestphall
    - CarlosBeckerWestphall
  abstract: >
    Cloud computing is a distributed computing model that still faces problems. New ideas emerge to take advantage of its features and among the research challenges found in the cloud, we can highlight Identity and Access Management. The main problems of the application of access control in the cloud are the necessary flexibility and scalability to support a large number of users and resources in a dynamic and heterogeneous environment, with collaboration and information sharing needs. This paper proposes the use of risk-based dynamic access control for cloud computing. The proposal is presented as an access control model based on an extension of the XACML standard with three new components: the Risk Engine, the Risk Quantification Web Services and the Risk Policies. The risk policies present a method to describe risk metrics and their quantification, using local or remote functions. The risk policies allow users and cloud service providers to define how to handle risk-based access control for their resources, using different quantification and aggregation methods. The model reaches the access decision based on a combination of XACML decisions and risk analysis. A prototype of the model is implemented, showing it has enough expressivity to describe the models of related work. In the experimental results, the prototype takes between 2 and 6 milliseconds to reach access decisions using a risk policy. A discussion on the security aspects of the model is also presented.
  destination: NOMS2014
  year: 2014
  doi: 10.1109/NOMS.2014.6838319
  urlNews: /news/2013/11/05/paper-accepted-at-noms-2014/

- id: SACMAT2014_ABAC
  id_iris: 226218
  title: Attribute Based Access Control for APIs in Spring Security
  authors:
    - AlessandroArmando
    - RobertoCarbone
    - EyasuGetahunChekole
    - SilvioRanise
  abstract: >
    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.
  destination: SACMAT2014
  year: 2014
  doi: 10.1145/2613087.2613109
  urlNews: /news/2014/05/20/papers-accepted-at-sacmat-2014/

- id: SACMAT2014_RBAC
  id_iris: 226016
  title: Scalable and Precise Automated Analysis of Administrative Temporal Role-Based Access Control
  authors:
    - SilvioRanise
    - TuanAnhTruong
    - AlessandroArmando
  abstract: >
    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.
  destination: SACMAT2014
  year: 2014
  doi: 10.1145/2613087.2613102
  urlNews: /news/2014/05/20/papers-accepted-at-sacmat-2014/

- id: SmartGridSec14
  id_iris: 251631
  title: Selective Release of Smart Metering Data in Multi-domain Smart Grids
  authors:
    - AlessandroArmando
    - RobertoCarbone
    - EyasuGetahunChekole
    - ClaudioPetrazzuolo
    - AndreaRanalli
    - SilvioRanise
  abstract: >
    In the context of energy efficiency, smart metering solutions are receiving growing attention as they support the automatic collection of (fine-grained) consumption data of appliances. While the capability of a stakeholder (such as a consumer, an utility, or a third-party service) to access smart metering data can give rise to innovative services for users, it makes the control of data release and usage significantly more complex. It is thus extremely important to put in place an adequate access control mechanism that takes into account the authorization requirements of the various stakeholders. To address this issue, we propose a framework based on the Attribute Based Access Control model for the selective release of smart metering data in cloud-based solutions for smart grids.
    We applied our framework to a scenario proposed by Energy@Home, a non-profit association of companies with the mission of developing and promoting techniques for energy efficiency in smart homes. As a proof of concept, we implemented our approach on top of the open-source Spring Security framework.
  destination: SmartGridSec14
  year: 2014
  doi: 10.1007/978-3-319-10329-7_4
  urlNews: /news/2014/02/19/paper-accepted-at-workshop-on-smart-grid-security/

- id: STM2014
  id_iris: 251431
  title: "ALPS: An Action Language for Policy Specification and Automated Safety Analysis"
  authors:
    - SilvioRanise
    - RiccardoTraverso
  abstract: >
    Authorization conditions of access control policies are complex and varied as they might depend, e.g., on the current time, the position of the users, selected parts of the system state, and even on the history of the computations. Several models, languages, and enforcement mechanisms have been proposed for different scenarios. Unfortunately, this complicates the verification of safety, i.e. no permission is leaked to unauthorized users. To avoid these problems, we present an intermediate language called Action Language for Policy Specification. Two desiderata drive its definition: (i) it should support as many models and policies as possible and (ii) it should be easily integrated in existing verification systems so that robust techniques (e.g., model checking or satisfiability solving) can be exploited to safety. We argue (i) by using selected examples of access control models and policies taken from the literature. For (ii), we prove some theoretical properties of the language that pave the way to the definition of automatic translations to available verification techniques.
  destination: STM2014
  year: 2014
  doi: 10.1007/978-3-319-11851-2_10

- id: TACAS2014
  id_iris: 211216
  title: "SATMC: A SAT-Based Model Checker for Security-Critical Systems"
  authors:
    - AlessandroArmando
    - RobertoCarbone
    - LucaCompagna
  abstract: >
    We present SATMC 3.0, a SAT-based bounded model checker for security-critical systems that stems from a successful combination of encoding techniques originally developed for planning with techniques developed for the analysis of reactive systems. SATMC has been successfully applied in a variety of application domains (security protocols, security-sensitive business processes, and cryptographic APIs) and for different purposes (design-time security analysis and security testing). SATMC strikes a balance between general purpose model checkers and security protocol analyzers as witnessed by a number of important success stories including the discovery of a serious man-in-the-middle attack on the SAML-based Single Sign-On (SSO) for Google Apps, an authentication flaw in the SAML 2.0 Web Browser SSO Profile, and a number of attacks on PKCS#11 Security Tokens. SATMC is integrated and used as back-end in a number of research prototypes (e.g., the AVISPA Tool, Tookan, the SPaCIoS Tool) and industrial-strength tools (e.g., the Security Validator plugin for SAP NetWeaver BPM).
  destination: TACAS2014
  year: 2014
  doi: 10.1007/978-3-642-54862-8_3

- id: TOCL2014
  id_iris: 264419
  title: Quantifier-free interpolation in combinations of equality interpolating theories
  authors:
    - RobertaBruttomesso
    - SilvioGhilardi
    - SilvioRanise
  abstract: >
    The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly reuse interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the strong (sub-)amalgamation property. Then, we provide an equivalent syntactic characterization and show that such characterization covers most theories commonly employed in verification. Finally, we design a combined quantifier-free interpolation algorithm capable of handling both convex and nonconvex theories; this algorithm subsumes and extends most existing work on combined interpolation.
  destination: TOCL
  destinationAddon: Volume 15, Issue 1, No. 5
  year: 2014
  doi: 10.1145/2490253

## 2015
- id: ASIACCS2015
  id_iris: 303737
  title: Automated Synthesis of Run-time Monitors to Enforce Authorization Policies in Business Processes
  authors:
    - ClaraBertolissi
    - DanielDosSantos
    - SilvioRanise
  destination: ASIACCS2015
  year: 2015
  doi: 10.1145/2714576.2714633
  urlNews: /news/2015/04/01/paper-accepted-at-asiaccs-2015/

- id: CNS2015
  id_iris: 303740
  title: Compiling NATO authorization policies for enforcement in the cloud and SDNs
  authors:
    - AlessandroArmando
    - SilvioRanise
    - RiccardoTraverso
    - KonradWrona
  destination: CNS2015
  year: 2015
  doi: 10.1109/CNS.2015.7346913

- id: DBSec2015
  id_iris: 303743
  title: Assisting the Deployment of Security-Sensitive Workflows by Finding Execution Scenarios
  authors:
    - DanielDosSantos
    - SilvioRanise
    - LucaCompagna
    - SerenaPonta
  destination: DBSec2015
  year: 2015
  doi: 10.1007/978-3-319-20810-7_6
  urlNews: /news/2015/04/21/paper-accepted-at-dbsec-2015/

- id: MIST2015
  id_iris: 303716
  title: Mobile App Security Assessment with the MAVeriC Dynamic Analysis Module
  authors:
    - AlessandroArmando
    - GianlucaBocci
    - GabrieleCosta
    - RoccoMammoliti
    - AlessioMerlo
    - SilvioRanise
    - RiccardoTraverso
    - AndreaValenza
  destination: DBSec2015
  year: 2015
  doi: 10.1007/978-3-319-20810-7_6
  urlNews: /news/2015/04/21/paper-accepted-at-dbsec-2015/

- id: POST2015
  id_iris: 303746
  title: Analysis of XACML Policies with SMT
  authors:
    - FatihTurkmen
    - JerryDenHartog
    - SilvioRanise
    - NicolaZannone
  destination: POST2015
  abstract: >
    The eXtensible Access Control Markup Language (XACML) is an extensible and flexible XML language for the specification of access control policies. However, the richness and flexibility of the language (along with the verbose syntax of XML) come with a price: errors are easy to make and difficult to detect when policies grow in size. If these errors are not detected and rectified, they can result in serious data leakage and/or privacy violations leading to significant legal and financial consequences. To assist policy authors in the analysis of their policies, several policy analysis tools have been proposed based on different underlying formalisms. However, most of these tools either abstract away functions over non-Boolean domains (hence they cannot provide information about them) or produce very large encodings which hinder the performance. In this paper, we present a generic policy analysis framework that employs SMT as the underlying reasoning mechanism. The use of SMT does not only allow more fine-grained analysis of policies but also improves the performance. We demonstrate that a wide range of security properties proposed in the literature can be easily modeled within the framework. A prototype implementation and its evaluation are also provided.
  year: 2015
  doi: 10.1007/978-3-662-46666-7_7

- id: SAC2015
  id_iris: 303755
  title: Automated analysis of RBAC policies with temporal constraints and static role hierarchies
  authors:
    - SilvioRanise
    - TuanAnhTruong
    - LucaViganò
  destination: SAC2015
  abstract: >
    Temporal role based access control models support the specification and enforcement of several temporal constraints on role enabling, role activation, and temporal role hierarchies among others. In this paper, we define three mappings that preserve the solutions to a class of policy problems (they map security analysis problems in presence of static temporal role hierarchies to problems without them) and we show how they can be used to extend the capabilities of a tool for the analysis of administrative temporal role-based access control policies to reason in presence of temporal role hierarchies. An experimental evaluation with a prototype implementation shows the better behavior of one of the proposed mappings over the other two. To the best of our knowledge, ours is the first tool capable of reasoning with (static) temporal role hierarchies.
  year: 2015
  doi: 10.1145/2695664.2695787

- id: SACMAT2015
  id_iris: 303728
  title: A SMT-based Tool for the Analysis and Enforcement of NATO Content-based Protection and Release Policies
  authors:
    - AlessandroArmando
    - SilvioRanise
    - RiccardoTraverso
    - KonradWrona
  destination: SACMAT2015
  year: 2015
  doi: 10.1145/2752952.2752954

- id: SECRYPT2015
  id_iris: 303758
  title: Modeling Authorization Policies for Web Services in Presence of Transitive Dependencies
  authors:
    - WorachetUttha
    - ClaraBertolissi
    - SilvioRanise
  destination: SECRYPT2015
  year: 2015
  doi: 10.5220/0005548502930300

- id: STM2015
  id_iris: 303761
  title: A Declarative Framework for Specifying and Enforcing Purpose-Aware Policies
  authors:
    - RiccardoDeMasellis
    - ChiaraGhidini
    - SilvioRanise
  destination: STM2015
  abstract: >
    Purpose is crucial for privacy protection as it makes users confident that their personal data are processed as intended. Available proposals for the specification and enforcement of purpose-aware policies are unsatisfactory for their ambiguous semantics of purposes and/or lack of support to the run-time enforcement of policies.
    In this paper, we propose a declarative framework based on a first-order temporal logic that allows us to give a precise semantics to purpose-aware policies and to reuse algorithms for the design of a run-time monitor enforcing purpose-aware policies. We also show the complexity of the generation and use of the monitor which, to the best of our knowledge, is the first such a result in literature on purpose-aware policies.
  year: 2015
  doi: 10.1007/978-3-319-24858-5_4

- id: TaPP2015
  title: A Proposal Architecture for Logical Data Tracking in Cloud
  authors:
    - MojtabaEskandari
    - BrunoCrispo
    - AndersonSantanaDeOliveira
  destination: TaPP2015
  year: 2015
  urlNews: /news/2015/06/05/paper-accepted-at-tapp-2015/

## 2016
- id: ABAC2016
  id_iris: 307012
  title: SMT-based Enforcement and Analysis of NATO Content-based Protection and Release Policies
  authors:
    - AlessandroArmando
    - SilvioRanise
    - RiccardoTraverso
    - KonradWrona
  destination: ABAC2016
  year: 2016
  doi: 10.1145/2875491.2875493
  urlNews: /news/2016/01/11/paper-accepted-at-abac-2016/

- id: ESSoS2016
  id_iris: 307090
  title: On the Security Cost of Using a Free and Open Source Component in a Proprietary Product
  authors:
    - StanislavDashevskyi
    - AchimBrucker
    - FabioMassacci
  abstract: >
    The work presented in this paper is motivated by the need to estimate the security effort of consuming Free and Open Source Software (FOSS) components within a proprietary software supply chain of a large European software vendor. To this extent we have identified three different cost models: centralized (the company checks each component and propagates changes to the different product groups), distributed (each product group is in charge of evaluating and fixing its consumed FOSS components), and hybrid (only the least used components are checked individually by each development team). We investigated publicly available factors (e. g., development activity such as commits, code size, or fraction of code size in different programming languages) to identify which one has the major impact on the security effort of using a FOSS component in a larger software product.
  destination: ESSoS2016
  year: 2016
  doi: 10.1007/978-3-319-30806-7_12
  urlNews: /news/2016/02/16/paper-accepted-at-essos-2016/

- id: FDSE2016
  id_iris: 307039
  title: "ASASPXL: New Clother for Analysing ARBAC Policies"
  authors:
    - TuanAnhTruong
    - SilvioRanise
  abstract: >
    Access Control is becoming increasingly important for today’s ubiquitous systems. In access control models, the administration of access control policies is an important task that raises a crucial analysis problem: if a set of administrators can give a user an unauthorized access permission. In this paper, we consider the analysis problem in the context of the Administrative Role-Based Access Control (ARBAC), one of the most widespread administrative models. We describe how we design heuristics to enable an analysis tool, called asaspXL, to scale up to handle large and complex ARBAC policies. An extensive experimentation shows that the proposed heuristics play a key role in the success of the analysis tool over the state-of-the-art analysis tools.
  destination: FDSE2016
  year: 2016
  doi: 10.1007/978-3-319-48057-2_19

- id: NDSS2016
  id_iris: 307029
  title: Attack Patterns for Black-Box Security Testing of Multi-Party Web Applications
  authors:
    - AvinashSudhodanan
    - AlessandroArmando
    - LucaCompagna
    - RobertoCarbone
  abstract: >
    The advent of Software-as-a-Service (SaaS) has led to the development of multi-party web applications (MPWAs). MPWAs rely on core trusted third-party systems (e.g., payment servers, identity providers) and protocols such as Cashier-as-aService (CaaS), Single Sign-On (SSO) to deliver business services to users. Motivated by the large number of attacks discovered against MPWAs and by the lack of a single general-purpose application-agnostic technique to support their discovery, we propose an automatic technique based on attack patterns for black-box, security testing of MPWAs. Our approach stems from the observation that attacks against popular MPWAs share a number of similarities, even if the underlying protocols and services are different. In this paper, we target six different replay attacks, a login CSRF attack and a persistent XSS attack. Firstly, we propose a methodology in which security experts can create attack patterns from known attacks. Secondly, we present a security testing framework that leverages attack patterns to automatically generate test cases for testing the security of MPWAs. We implemented our ideas on top of OWASP ZAP (a popular, open-source penetration testing tool), created seven attack patterns that correspond to thirteen prominent attacks from the literature and discovered twenty one previously unknown vulnerabilities in prominent MPWAs (e.g., twitter.com, developer.linkedin.com, pinterest.com), including MPWAs that do not belong to SSO and CaaS families.
  destination: NDSS2016
  year: 2016
  urlNews: /news/2015/10/23/paper-accepted-at-ndss-2016/

- id: RTSI2016
  id_iris: 313241
  title: "A delegated authorization solution for smart-city mobile applications"
  authors:
    - GiadaSciarretta
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    An increasingly popular scenario for Smart Cities is the one in which mobile apps attempt to access resources (e.g., open data about public transportation or e-government services) made available by city authorities through the use of Application Programming Interfaces (APIs). There is a growing awareness of the benefits of using APIs to foster civic engagement through a more efficient and personalized delivery of government services, and as an enabler of a new wave of innovation contributing to a more automated and sustainable city functioning. Despite these advantages, there are several factors hindering the exploitation of APIs. One of the most important technical barriers to the creation of mobile apps following the recurrent pattern of consuming data (e.g., selected parts of open data or user profiles) stored by other applications or services is the lack of a secure delegation mechanism. In this paper, we discuss the main security issues underlying the design of such a delegation mechanism for Smart City mobile apps and present a solution-based on OAuth 2.0-overcoming the security problems. An implementation of the solution has been integrated in the Smart Community Platform for developing open services in the Trentino region and is being used daily by up to 13,000 users. To date, no security issue has been reported.
  destination: RTSI2016
  year: 2016
  doi: 10.1109/RTSI.2016.7740623

- id: SACMAT2016
  id_iris: 307044
  title: Modular Synthesis of Enforcement Mechanisms for the Workflow Satisfiability Problem
  authors:
    - DanielDosSantos
    - SerenaPonta
    - SilvioRanise
  abstract: >
    Modularity is an important concept in the design and enactment of workflows. However, supporting the specification and enforcement of authorization in this setting is not straightforward. In this paper, we introduce a notion of component and a combination mechanism for security-sensitive workflows. These are business processes in which execution constraints on the tasks are complemented with authorization constraints (e.g., Separation of Duty) and authorization policies (specifying which users can execute which tasks). We show how authorization constraints can also be imposed across components and demonstrate the usefulness of our notion of component by showing (i) the scalability of a technique for the synthesis of run-time monitors for security-sensitive workflows; and (ii) the design of a plug-in for the reuse of workflows and related run-time monitors inside an editor for security-sensitive workflows.
  destination: SACMAT2016
  year: 2016
  doi: 10.1145/2914642.2914649

- id: SECRYPT2016
  id_iris: 307033
  title: "Security of Mobile Single Sign-On: a Rational Reconstruction of Facebook Login Solution"
  authors:
    - GiadaSciarretta
    - AlessandroArmando
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    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.
  destination: SECRYPT2016
  year: 2016
  doi: 10.5220/0005969001470158
  urlNews: /news/2016/06/16/paper-accepted-at-secrypt-2016/

- id: STTT2016
  id_iris: 307037
  title: Parameterized model checking for security policy analysis
  authors:
    - SilvioRanise
    - RiccardoTraverso
    - TuanAnhTruong
  abstract: >
    We explain how a parameterized model checking technique can be exploited to mechanize the analysis of access control policies. The main advantage of the approach is to reason regardless of the number of users of the system in which the policy is enforced. This permits to obtain more useful results from the analysis; for instance, ensuring that sensitive permissions cannot be leaked regardless of the number of users in the system. We also briefly discuss how some heuristics make the technique scalable to handle (very) large policies. This is demonstrated by a comparative experimental evaluation with state-of-the-art tools for the analysis of access control policies.
  destination: STTT
  year: 2016
  doi: 10.1007/s10009-015-0410-1

- id: TACAS2016
  id_iris: 307053
  title: "Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-Sensitive Business Processes"
  authors:
    - LucaCompagna
    - DanielDosSantos
    - SerenaPonta
    - SilvioRanise
  abstract: >
    Cerberus is a tool to automatically synthesize run-time enforcement mechanisms for security-sensitive Business Processes (BPs). The tool is capable of guaranteeing that the execution constraints ECEC on the tasks together with the authorization policy APAP and the authorization constraints ACAC are satisfied while ensuring that the process can successfully terminate. Cerberus can be easily integrated in many workflow management systems, it is transparent to process designers, and does not require any knowledge beyond usual BP modeling. The tool works in two phases. At design-time, the enforcement mechanism M, parametric in the authorization policy APAP, is generated from ECEC and ACAC; M can thus be used with any instance of the same BP provided that ECEC and ACAC are left unchanged. At run-time, a specific authorization policy is added to M, thereby obtaining an enforcement mechanism M∗M∗ dedicated to a particular instance of the security-sensitive business process. To validate our approach, we discuss the implementation and usage of Cerberus in the SAP HANA Operational Intelligence platform.
  destination: TACAS2016
  year: 2016
  doi: 10.1007/978-3-662-49674-9_36

## 2017
- id: CODASPY2017
  id_iris: 313213
  title: "Aegis: Automatic Enforcement of Security Policies in Workflow-driven Web Applications"
  authors:
    - LucaCompagna
    - DanielDosSantos
    - SerenaPonta
    - SilvioRanise
  abstract: >
    Organizations often expose business processes and services as web applications. Improper enforcement of security policies in these applications leads to business logic vulnerabilities that are hard to find and may have dramatic security implications. Aegis is a tool to automatically synthesize run-time monitors to enforce control-flow and data-flow integrity, as well as authorization policies and constraints in web applications. The enforcement of these properties can mitigate attacks, e.g., authorization bypass and workflow violations, while allowing regulatory compliance in the form of, e.g., Separation of Duty. Aegis is capable of guaranteeing business continuity while enforcing the security policies. We evaluate Aegis on a set of real-world applications, assessing the enforcement of policies, mitigation of vulnerabilities, and performance overhead.
  destination: CODASPY2017
  year: 2017
  doi: 10.1145/3029806.3029813

- id: COSE2017
  id_iris: 313200
  title: "Anatomy of the Facebook solution for mobile single sign-on: Security assessment and improvements"
  authors:
    - GiadaSciarretta
    - RobertoCarbone
    - SilvioRanise
    - AlessandroArmando
  abstract: >
    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 abstract model and a related implementation capable of solving the identified vulnerabilities and accommodating any Identity Provider. Finally, we have analyzed the new native SSO solution proposed by the OAuth Working Group, extracted the related abstract model and made a comparison with our proposal.
  destination: COSE
  destinationAddon: Volume 71, November 2017, Pages 71-86
  year: 2017
  doi: 10.1016/j.cose.2017.04.011

- id: COSE2017_XACML
  id_iris: 313198
  title: Formal analysis of XACML policies using SMT
  authors:
    - FatihTurkmen
    - JerryDenHartog
    - SilvioRanise
    - NicolaZannone
  abstract: >
    The eXtensible Access Control Markup Language (XACML) has attracted significant attention from both industry and academia, and has become the de facto standard for the specification of access control policies. However, its XML-based verbose syntax and rich set of constructs make the authoring of XACML policies difficult and error-prone. Several automated tools have been proposed to analyze XACML policies before their actual deployment. However, most of the existing tools either cannot efficiently reason about non-Boolean attributes, which often appear in XACML policies, or restrict the analysis to a small set of properties. This work presents a policy analysis framework for the verification of XACML policies based on SAT modulo theories (SMT). We show how XACML policies can be encoded into SMT formulas, along with a query language able to express a variety of well-known security properties, for policy analysis. By being able to reason over non-Boolean attributes, our SMT-based policy analysis framework allows a fine-grained policy analysis while relieving policy authors of the burden of defining an appropriate level of granularity of the analysis. An evaluation of the framework shows that it is computationally efficient and requires less memory compared to existing approaches.
  destination: COSE
  destinationAddon: Volume 66, May 2017, Pages 185-203
  year: 2017
  doi: 10.1016/j.cose.2017.01.009

- id: EUROSP2017
  id_iris: 313216
  title: "Large-scale Analysis & Detection of Authentication Cross-Site Request Forgeries"
  authors:
    - AvinashSudhodanan
    - RobertoCarbone
    - LucaCompagna
    - NicolasDolgin
    - AlessandroArmando
    - UmbertoMorelli
  abstract: >
    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.
  destination: EUROSP2017
  year: 2017
  doi: 10.1109/EuroSP.2017.45
  urlNews: /news/2017/10/17/paper-accepted-at-eurosp-2017/

- id: IFIPSEC2017
  id_iris: 313224
  title: "Assisted Authoring, Analysis and Enforcement of Access Control Policies in the Cloud"
  authors:
    - UmbertoMorelli
    - SilvioRanise
  abstract: >
    The heterogeneity of cloud computing platforms hinders the proper exploitation of cloud technologies since it prevents interoperability, promotes vendor lock-in and makes it very difficult to exploit the well-engineered security mechanisms made available by cloud providers. In this paper, we introduce a technique to help developers to specify and enforce access control policies in cloud applications. The main idea is twofold. First, use a high-level specification language with a formal semantics that allows to answer access requests abstracting from an access control mechanism available in a particular cloud platform. Second, exploit an automated translation mechanism to compute (equivalent) policies that can be enforced in two of the most widely used cloud platforms: AWS and Openstack. We illustrate the technique on a running example and report our experience with a prototype implementation. 
  destination: IFIPSEC2017
  year: 2017
  doi: 10.1007/978-3-319-58469-0_20
  urlNews: /news/2017/06/15/paper-accepted-at-ifipsec-2017/

- id: JCS2017
  id_iris: 313204
  title: Automatically finding execution scenarios to deploy security-sensitive workflows
  authors:
    - DanielDosSantos
    - SilvioRanise
    - LucaCompagna
    - SerenaPonta
  abstract: >
    We introduce a new class of analysis problems, called Scenario Finding Problems (SFPs), for security-sensitive business processes that – besides execution constraints on tasks – define access control policies (constraining which users can execute which tasks) and authorization constraints (such as Separation of Duty). The solutions to SFPs are concrete execution scenarios that assist customers in the reuse and deployment of security-sensitive workflows. We study the relationship of SFPs to well-known properties of security-sensitive processes such as Workflow Satisfiability and Resiliency together with their complexity. Finally, we present a symbolic approach to solving SFPs and describe our experience with a prototype implementation on real-world business process models taken from an on-line library.
  destination: JCS
  destinationAddon: Volume 25, no. 3, Pages 255-282
  year: 2017
  doi: 10.3233/JCS-16894

- id: SACMAT2017
  id_iris: 313220
  title: "Security Analysis and Legal Compliance Checking for the Design of Privacy-friendly Information Systems"
  authors:
    - PaoloGuarda
    - SilvioRanise
    - HariSiswantoro
  abstract: >
    Nowadays, most of business practices involve personal data-processing of customers and employees. This is strictly regulated by legislation to protect the rights of the data subject. Enforcing regulation into enterprise information system is a non-trivial task that requires an interdisciplinary approach. This paper presents a declarative framework to support the specification of information system designs, purpose-aware access control policies, and the legal requirements derived from the European Data Protection Directive. This allows for compliance checking via a reduction to policy refinement that is supported by available automated tools. We briefly discuss the results of the compliance analysis with a prototype tool on a simple but realistic scenario about the processing of personal data to produce salary slips of employees in an Italian organization.
  destination: SACMAT2017
  year: 2017
  doi: 10.1145/3078861.3078879

- id: SAFECOMP2017
  id_iris: 313237
  title: "Automated Legal Compliance Checking by Security Policy Analysis"
  authors:
    - SilvioRanise
    - HariSiswantoro
  abstract: >
    Legal compliance-by-design is the process of developing a software system that processes personal data in such a way that its ability to meet specific legal provisions is ascertained. In this paper, we describe techniques to automatically check the compliance of the security policies of a system against formal rules derived from legal provisions by re-using available tools for security policy verification. We also show the practical viability of our approach by reporting the experimental results of a prototype for checking compliance of realistic and synthetic policies against the European Data Protection Directive (EU DPD).
  destination: SAFECOMP2017
  year: 2017
  doi: 10.1007/978-3-319-66284-8_30
  
- id: SECRYPT2017
  id_iris: 313202
  title: "Strong Authentication for e-Banking: a Survey on European Regulations and Implementations"
  authors:
    - FedericoSinigaglia
    - GabrieleCosta
    - RobertoCarbone
  abstract: >
    The modern, smart society needs a reliable and trustworthy access to the internet of services. Strong authentication mechanisms promise to rise the bar of security and they are polarizing the attention of both institutional and industrial stakeholders. In this survey we take stock of the strong authentication mechanisms used by e-Banking services in terms of regulations and implementations. To this aim, we reviewed the EU regulation and its evolution in the last decade. Moreover, we analyzed the strong authentication mechanisms implemented by 26 major EU and non-EU banks.
  destination: SECRYPT2017
  year: 2017
  doi: 10.5220/0006438504800485
  urlNews: /news/2017/06/15/paper-accepted-at-secrypt-2017/

- id: SEFM2017
  id_iris: 313228
  title: On Run-Time Enforcement of Authorization Constraints in Security-Sensitive Workflows
  authors:
    - DanielDosSantos
    - SilvioRanise
  abstract: >
    In previous work, we showed how to use an SMT-based model checker to synthesize run-time enforcement mechanisms for business processes augmented with access control policies and authorization constraints, such as Separation of Duties. The synthesized enforcement mechanisms are able to guarantee both termination and compliance to security requirements, i.e. solving the run-time version of the Workflow Satisfiability Problem (WSP). No systematic approach to specify the various constraints considered in the WSP literature has been provided. In this paper, we first propose a classification of these constraints and then show how to encode them in the declarative input language of the SMT-based model checker used for synthesis. This shows the flexibility of the SMT approach to solve the run-time version of the WSP in presence of different authorization constraints.
  destination: SEFM2017
  year: 2017
  doi: 10.1007/978-3-319-66197-1_13

- id: TLDKS2017
  id_iris: 313210
  title: Scalable Automated Analysis of Access Control and Privacy Policies
  authors:
    - TuanAnhTruong
    - SilvioRanise
    - ThanhTungNguyen
  abstract: >
    Access Control is becoming increasingly important for today ubiquitous systems. Sophisticated security requirements need to be ensured by authorization policies for increasingly complex and large applications. As a consequence, designers need to understand such policies and ensure that they meet the desired security constraints while administrators must also maintain them so as to comply with the evolving needs of systems and applications. These tasks are greatly complicated by the expressiveness and the dimensions of the authorization policies. It is thus necessary to provide policy designers and administrators with automated analysis techniques that are capable to foresee if, and under what conditions, security properties may be violated. In this paper, we consider this analysis problem in the context of the Role-Based Access Control (RBAC), one of the most widespread access control models. We describe how we design heuristics to enable an analysis tool, called asaspXL, to scale up to handle large and complex Administrative RBAC policies. We also discuss the capability of applying the techniques inside the tool to the analysis of location-based privacy policies. An extensive experimentation shows that the proposed heuristics play a key role in the success of the analysis tool over the state-of-the-art analysis tools.
  destination: TLDKS
  destinationAddon: Volume XXXVI
  year: 2017
  doi: 10.1007/978-3-662-56266-6_7

- id: WiSec2017
  id_iris: 313230
  title: Toward secure and efficient attestation for highly dynamic swarms
  authors:
    - MorenoAmbrosin
    - MauroConti
    - RiccardoLazzaretti
    - MdMasoomRabbani
    - SilvioRanise
  abstract: >
    Remote Attestation (RA) has been proven to be a powerful security service to check the legitimacy of the software configuration (e.g., running software and data) of devices. In recent years, advances in trusted computing, made possible to extend the use of RA also to embedded and Internet of Things (IoT) devices. The massive scale of IoT deployments poses scalability challenges to RA. Recently, researchers proposed efficient protocols for collective network attestation, i.e., efficient attestation of a whole network of interconnected embedded devices; however, most of these solutions are either costly, or simply unsuitable for highly dynamic networks. This paper presents our ongoing effort in the definition of an efficient, scalable and secure solution for collective attestation of potentially large and highly dynamic networks of tiny devices.
  destination: WiSec2017
  year: 2017
  doi: 10.1145/3098243.3106026

## 2018
- id: FPS2018
  id_iris: 316195
  title: Validating Requirements of Access Control for Cloud-Edge IoT Solutions
  authors:
    - TahirAhmad
    - SilvioRanise
  abstract: >
    The pervasiveness of Internet of Things (IoT) solutions have stimulated research on the basic security mechanisms needed in the wide range of IoT use case scenarios, ranging from home automation to industrial control systems. We focus on access control for cloud-edge based IoT solutions for which—in previous work—we have proposed a lazy approach to Access Control as a Service for the specification, administration, and enforcement of policies. The validity of the approach was evaluated in a realistic smart-lock scenario. In this paper, we argue that the approach is adaptable to a wide range of IoT use case scenarios by validating the requirements elicited when analyzing the smart lock scenario.
  destination: FPS2018
  year: 2018
  doi: 10.1007/978-3-030-18419-3_9
  urlNews: /news/2018/10/11/paper-accepted-at-fps-2018/

- id: JCS2018
  id_iris: 316172
  title: Automated and efficient analysis of administrative temporal RBAC policies with role hierarchies 
  authors:
    - SilvioRanise
    - TuanAnhTruong
    - LucaViganò
  destination: JCS
  year: 2018
  doi: 10.3233/JCS-15756

- id: PIM2018
  id_iris: 320660
  title: Design and Security Assessment of Usable Multi-factor Authentication and Single Sign-On Solutions for Mobile Applications
  authors:
    - RobertoCarbone
    - SilvioRanise
    - GiadaSciarretta
  abstract: >
    In this interactive workshop we focused on multi-factor authentication and Single Sign-On solutions for mobile native applications. The main objective was to create awareness of the current limitations of these solutions in the mobile context. Thus, after an introduction part, the participants were invited to discuss usability and security issues of different mobile authentication scenarios. After this interactive part, we concluded the workshop presenting our on-going work on this topic by briefly describing our methodology for the design and security assessment of multi-factor authentication and Single Sign-On solutions for mobile native applications; and presenting a plugin that helps developers make their mobile native application secure.
  destination: PIM2018
  year: 2018
  doi: 10.1007/978-3-030-16744-8_4

- id: POST2018
  id_iris: 316182
  title: "Design, Formal Specification and Analysis of Multi-Factor Authentication Solutions with a Single Sign-On Experience"
  authors:
    - GiadaSciarretta
    - RobertoCarbone
    - SilvioRanise
    - LucaViganò
  abstract: >
    Over the last few years, there has been an almost exponential increase of the number of mobile applications that deal with sensitive data, such as applications for e-commerce or health. When dealing with sensitive data, classical authentication solutions based on username-password pairs are not enough, and multi-factor authentication solutions that combine two or more authentication elements of different categories are required. Many different such solutions are available, but they usually cover the scenario of a user accessing web applications on their laptops, whereas in this paper we focus on native mobile applications. This changes the exploitable attack surface and thus requires a specific analysis. In this paper, we present the design, the formal specification and the security analysis of a solution that allows users to access different mobile applications through a multi-factor authentication solution providing a Single Sign-On experience. The formal and automated analysis that we performed validates the security goals of the solution we propose.
  destination: POST2018
  year: 2018
  doi: 10.1007/978-3-319-89722-6_8
  urlNews: /news/2018/01/25/paper-accepted-at-post-2018/

- id: SACMAT2018
  id_iris: 316176
  title: "A Lazy Approach to Access Control as a Service (ACaaS) for IoT: An AWS Case Study"
  authors:
    - TahirAhmad
    - UmbertoMorelli
    - SilvioRanise
    - NicolaZannone
  abstract: >
    The Internet of Things (IoT) is receiving considerable attention from both industry and academia because of the new business models that it enables and the new security and privacy challenges that it generates. Major Cloud Service Providers (CSPs) have proposed platforms to support IoT by combining cloud and edge computing. However, the security mechanisms available in the cloud have been extended to IoT with some shortcomings with respect to the management and enforcement of access control policies. Access Control as a Service (ACaaS) is emerging as a solution to overcome these difficulties. The paper proposes a lazy approach to ACaaS that allows the specification and management of policies independently of the CSP while leveraging its enforcement mechanisms. We demonstrate the approach by investigating (also experimentally) alternative deployments in the IoT platform offered by Amazon Web Services on a realistic smart lock solution.
  destination: SACMAT2018
  year: 2018
  doi: 10.1145/3205977.3205989
  urlNews: /news/2018/04/02/paper-accepted-at-sacmat-2018/

- id: SACMAT2018_Satisfiability
  id_iris: 316174
  title: Solving Multi-Objective Workflow Satisfiability Problems with Optimization Modulo Theories Techniques
  authors:
    - ClaraBertolissi
    - DanielDosSantos
    - SilvioRanise
  destination: SACMAT2018
  year: 2018
  doi: 10.1145/3205977.3205982

- id: SIoT2018
  id_iris: 316309
  title: "PADS: Practical Attestation for Highly Dynamic Swarm Topologies"
  authors:
    - MdMasoomRabbani
    - SilvioRanise
  destination: SIoT2018
  year: 2018
  doi: 10.1109/SIoT.2018.00009

- id: SSPIM2018
  title: "Secure and Usable Mobile Solutions for Authentication and Single Sign-On: a Methodology for their Design and Assessment"
  authors:
    - RobertoCarbone
    - SilvioRanise
    - GiadaSciarretta
  abstract: >
    The widespread use of digital identities in our everyday life, along with the release of our sensitive data on many online transactions, calls for Identity Management (IdM) solutions that are secure, usable, privacy-aware, and compatible with new technologies, such as mobile and cloud. While there exist many secure IdM solutions for web applications, their adaptation in the mobile context is a new and open challenge. Due to the lack of specifications and security guidelines, designing a mobile IdM solution that covers different authentication aspects from scratch is not a simple task; and as its security depends on several trust and communication assumptions, in most cases, could result in a solution with hidden vulnerabilities. To overcome this difficulty, we provide a reference model and a design methodology which can be used by different organizations to implement mobile Single Sign-On and multi-factor authentication. Main objectives of the workshop are to create awareness of privacy and security issues together with legal provisions related to authentication in mobile computing and perform an experimental evaluation of security vs usability of widespread second-factor authentication solutions for mobile applications.
  destination: SSPIM2018
  year: 2018
  urlComplementary: /complementary/SSPIM2018

- id: WiMob2018
  id_iris: 316311
  title: "SPLIT: A Secure and Scalable RPL routing protocol for Internet of Things"
  authors:
    - MauroConti
    - PallaviKaliyar
    - MdMasoomRabbani
    - SilvioRanise
  abstract: >
    Due to recent notorious security threats, like Mirai-botnet, it is challenging to perform efficient data communication and routing in low power and lossy networks (LLNs) such as Internet of Things (IoT), in which huge data collection and processing are predictable. The Routing Protocol for low power and Lossy networks (RPL) is recently standardized as a routing protocol for LLNs. However, the lack of scalability and the vulnerabilities towards various security threats still pose a significant challenge in the broader adoption of RPL in LLNs.To address these challenges, we propose SPLIT, a secure and scalable RPL routing protocol for IoT networks. SPLIT effectively uses a lightweight remote attestation technique to ensure software integrity of network nodes. To avoid additional overhead caused by attestation messages, SPLIT piggybacks attestation process on the RPL's control messages. Thus, SPLIT enjoys the low energy consumption and scalability features of RPL protocol, which are essential in resource-constrained large scale networks such as IoT. The simulation results for different IoT scenarios show the effectiveness of SPLIT compared to the state-of-the-art in presence of different types of attacks, concerning metrics such as packet delivery ratio and energy consumption.
  destination: SIoT2018
  year: 2018
  doi: 10.1109/SIoT.2018.00009

## 2019
- id: MSTEC2019
  id_iris: 321967
  title: "An Open and Flexible CyberSecurity Training Laboratory in IT/OT Infrastructures"
  authors:
    - UmbertoMorelli
    - SilvioRanise
    - LorenzoNicolodi
  abstract: >
    There are significant concerns regarding the lack of proficient cybersecurity professionals with a background in both Information Technology (IT) and Operational Technology (OT). To alleviate this problem, we propose an open and flexible laboratory for experimenting with an IT/OT infrastructure and the related cybersecurity problems, such as emulating attacks and understanding how they work and how they could be identified and mitigated. We also report our experience in using the laboratory during a one-week training event with 24 students from 7 different high-schools at the mechatronics prototyping facility ProM in Rovereto (Italy).
  destination: MSTEC2019
  year: 2019
  doi: 10.1007/978-3-030-42051-2_10
  urlNews: /news/2019/08/06/paper-accepted-at-mstec-2019/

- id: IEEESERVICES2019
  id_iris: 320696
  title: "MQTTSA: A Tool for Automatically Assisting the Secure Deployments of MQTT brokers"
  authors:
    - AndreaPalmieri
    - PaoloPrem
    - SilvioRanise
    - UmbertoMorelli
    - TahirAhmad
  abstract: >
    The Internet of Things (IoT) is radically changing the way people live and interact with society: ranging from wearables to smart cities, the number of IoT devices has grown exponentially. The Message Queuing Telemetry Transport (MQTT) protocol is one of the most widely used IoT communication protocols. However, our investigation over publicly available MQTT endpoints confirms an alarming trend, i.e. many do not provide adequate security measures and often rely on the insecure default configuration. To improve the security awareness on the use of MQTT the paper presents MQTT Security Assistant (MQTTSA), a tool that automatically detects misconfigurations in MQTT-based IoT deployments. To assist IoT system developers, MQTTSA produces a report outlining detected vulnerabilities, together with (high level) hints and code snippets to implement adequate mitigations. The effectiveness of the tool is assessed by a thorough experimental evaluation.
  destination: IEEESERVICES2019
  year: 2019
  doi: 10.1109/SERVICES.2019.00023
  urlNews: /news/2019/05/04/paper-accepted-at-ieee-services-2019/

- id: DBSec2019_TLSA
  id_iris: 320466
  title: "Lost in TLS? No More! Assisted Deployment of Secure TLS Configurations"
  authors:
    - SalvatoreManfredi
    - SilvioRanise
    - GiadaSciarretta
  abstract: >
    Over the last few years, there has been an almost exponential growth of TLS popularity and usage, especially among applications that deal with sensitive data. However, even with this widespread use, TLS remains for many system administrators a complex subject. The main reason is that they do not have the time to understand all the cryptographic algorithms and features used in a TLS suite and their relative weaknesses. For these reasons, many different tools have been developed to verify TLS implementations. However, they usually analyze the TLS configuration and provide a list of possible attacks, without specifying their mitigations. In this paper, we present TLSAssistant, a fully-featured tool that combines state-of-the-art TLS analyzers with a report system that suggests appropriate mitigations and shows the full set of viable attacks.
  destination: DBSec2019
  destinationAddon: vol. 11559, pp. 201-220
  year: 2019
  doi: 10.1007/978-3-030-22479-0_11
  urlNews: /news/2019/04/15/paper-accepted-at-dbsec-2019/

- id: ETAA2019_MuFASA
  id_iris: 325074
  title: "MuFASA: A Tool for High-level Specification and Analysis of Multi-factor Authentication Protocols"
  authors:
    - FedericoSinigaglia
    - RobertoCarbone
    - GabrieleCosta
    - SilvioRanise
  abstract: >
    In recent years, the usage of online services (e.g., banking) has considerably increased. To protect the sensitive resources managed by these services against attackers, Multi-Factor Authentication (MFA) has been widely adopted. To date, a variety of MFA protocols have been implemented, leveraging different designs and features and providing a non-homogeneous level of security and user experience. Public and private authorities have defined laws and guidelines to guide the design of more secure and usable MFA protocols, but their influence on existing MFA implementations remains unclear.
    We present MuFASA, a tool for high-level specification and analysis of MFA protocols, which aims at supporting normal users and security experts (in the design phase of an MFA protocol), providing a high level report regarding possible risks associated to the specified MFA protocol, its resistance to a set of attacker models (defined by NIST), its ease-of-use and its compliance with a set of security requirements derived from European laws.
  destination: ETAA2019
  year: 2019
  doi: 10.1007/978-3-030-39749-4_9
  urlComplementary: /tools/MuFASA
  urlNews: /news/2019/07/30/paper-accepted-at-etaa-2019/

- id: FPS2019
  id_iris: 324208
  title: "Enroll, and authentication will follow: eID-based enrollment for a customized, secure, and frictionless authentication experience"
  authors:
    - SilvioRanise
    - GiadaSciarretta
    - AlessandroTomasi
  destination: FPS2019
  year: 2019
  doi: 10.1007/978-3-030-45371-8_10
  urlNews: /news/2019/10/01/paper-accepted-at-fps-2019/

- id: GCIoT2019
  id_iris: 325066
  title: Blockchain Tree for eHealth
  authors:
    - SergiiKushch
    - SilvioRanise
    - GiadaSciarretta
  destination: GCIoT2019
  year: 2019
  doi: 10.1109/GCIoT47977.2019.9058412

- id: IoTBDS2019
  id_iris: 320694
  title: "Learning from Others' Mistakes: An Analysis of Cyber-security Incidents"
  authors:
    - GiovanniMariaAbbiati
    - SilvioRanise
    - AntonioSchizzerotto
    - AlbertoSiena
  destination: IoTBDS2019
  year: 2019
  doi: 10.5220/0007721202990306

- id: MicroIDGym_2019
  id_iris: 325776
  title: "Micro-Id-Gym: Identity Management Workouts with Container-Based Microservices"
  authors:
    - AndreaBisegna
    - RobertoCarbone
    - IvanMartini
    - ValentinaOdorizzi
    - GiulioPellizzari
    - SilvioRanise
  destination: IJISC
  destinationAddon: Volume 8, Issue 1
  year: 2019
  doi: 10.19107/IJISC.2019.01.06

- id: SECRYPT2019_DP
  id_iris: 320692
  title: A Tool-assisted Methodology for the Data Protection Impact Assessment
  authors:
    - SalimehDashti
    - SilvioRanise
  abstract: >
    We propose a pragmatic methodology to the Data Protection Impact Assessment (DPIA) based on a tool capable of assisting users during crucial activities such as data processing specification and risk analysis. Previous work on compliance checking and our experience in developing a DPIA methodology for the Public Administration of the province of Trento in Italy are the basis of this work.
  destination: SECRYPT2019
  year: 2019
  doi: 10.5220/0007932202760283
  urlNews: /news/2019/05/02/papers-accepted-at-secrypt-2019/

- id: SECRYPT2019_SSO
  id_iris: 319672
  title: A Wizard-Based Approach for Secure Code Generation of Single Sign-On and Access Delegation Solutions for Mobile Native Apps
  authors:
    - AmirSharif
    - RobertoCarbone
    - SilvioRanise
    - GiadaSciarretta
  abstract: >
    Many available mobile applications (apps) have poorly implemented Single Sign-On and Access Delegation solutions leading to serious security issues. This could be caused by inexperienced developers who prioritize the implementation of core functionalities and/or misunderstand security critical parts. The situation is even worse in complex API scenarios where the app interacts with several providers. To address these problems, we propose a novel wizard-based approach that guides developers to integrate multiple third-party Identity Management (IdM) providers in their apps, by (i) “enforcing” the usage of best practices for native apps, (ii) avoiding the need to download several SDKs and understanding their online documentations (a list of known IdM providers with their configuration information is embedded within our approach), and (iii) automatically generating the code to enable the communication with the different IdM providers. The effectiveness of the proposed approach has been assessed by implementing an Android Studio plugin and using it to integrate several IdM providers, such as OKTA, Auth0, Microsoft, and Google.
  destination: SECRYPT2019
  year: 2019
  doi: 10.5220/0007930502680275
  urlComplementary: /complementary/SECRYPT2019_SSO
  urlNews: /news/2019/05/02/papers-accepted-at-secrypt-2019/

- id: STM2019
  id_iris: 320526
  title: "Audit-Based Access Control with a Distributed Ledger: Applications to Healthcare Organizations"
  authors:
    - UmbertoMorelli
    - SilvioRanise
    - DamianoSartori
    - GiadaSciarretta
    - AlessandroTomasi
  abstract: >
    We propose an audit-based architecture that leverages the Hyperledger Fabric distributed ledger as a means to increase accountability and decentralize the authorization decision process of Attribute-Based Access Control policies by using smart contracts. Our goal is to decrease the trust in administrators and users with privileged accounts, and make the a posteriori verification of access events more reliable. We implement our approach to the use case of Electronic Health Record access control. Preliminary experiments show the viability of the proposed approach.
  destination: STM2019
  year: 2019
  doi: 10.1007/978-3-030-31511-5_2
  urlNews: /news/2019/07/25/paper-accepted-at-stm-2019/

## 2020
- id: 5GWF20
  id_iris: 323486
  title: "Security Considerations on 5G-Enabled Back-Situation Awareness for CCAM"
  authors:
    - MarcoCentenaro
    - StefanoBerlato
    - RobertoCarbone
    - GianfrancoBurzio
    - GiuseppeFarandaCordella
    - SilvioRanise
    - RobertoRiggio
  abstract: >
    The increasing demand for cooperative, connected, and automated mobility (CCAM) services should proceed at the same pace with the enforcement of security mechanisms that would make CCAM services secure. The first contribution of this paper resides in a review of the ongoing regulatory and standardization activities related to cybersecurity of autonomous vehicles. Then, referring to the ongoing piloting activities funded by the European Union, we focus on the security threats for back-situation awareness (BSA), i.e., a safety-related CCAM service dealing with emergency scenarios. We propose a practical strong authentication method for BSA, and extensively discuss how existing standards can mitigate the security threats of this prominent CCAM service.
  destination: 5GWF20
  year: 2020
  urlNews: /news/2020/07/20/paper-accepted-at-5GWF20/

- id: AHN2020
  id_iris: 323806
  title: Attestation-enabled secure and scalable routing protocol for IoT networks
  authors:
    - MauroConti
    - PallaviKaliyar
    - MdMasoomRabbani
    - SilvioRanise
  abstract: >
    Cybercrime in the past decade has experienced an all-time high due to the inclusion of so-called smart devices in our daily lives. These tiny devices with brittle security features are often dubbed as the Internet of Things (IoT). Their inclusion is not only limited to our daily lives but also in different fields, for example, healthcare, smart-industries, aviation, and smart-cities. Although IoT devices make our lives easy and perform our jobs in a smart way, but their fragile security mechanisms pose a severe challenge regarding safety and privacy of its users. Attacks like Stuxnet, and Mirai-botnet are the key examples of the damages that can be caused by maliciously controlling these devices. One effective tool to identify a malicious entity at a network device is to perform Remote Attestation (RA). However, performing RA over a large, heterogeneous IoT network is difficult tasks due to resource constrain nature of these networks. To this end, we propose a novel scheme called SARP, which is an attestation-assisted secure and scalable routing protocol for IoT networks. SARP performs attestation in large scale IoT networks by using Routing Protocol for Low Power and Lossy Networks (RPL) framework and exploiting the inbuilt features of RPL. In particular, SARP uses attestation technique that not only secures the network from internal attacks, but it also provides security to RPL’s data communication process, which helps to improve the overall network performance. Moreover, SARP supports network mobility, device heterogeneity, and network scalability, while it does not sacrifice the key requirements of IoT networks such as low energy and memory consumption, and low network overhead. The simulation results obtained in different IoT scenarios in presence of various types of attacks show the effectiveness of SARP, concerning energy consumption, packet delivery ratio, network overhead, data integrity, and communication security.
  destination: AHN
  year: 2020
  doi: 10.1016/j.adhoc.2019.102054

- id: ASIACCS2020
  id_iris: 323366
  title: "Exploring Architectures for Cryptographic Access Control Enforcement in the Cloud for Fun and Optimization"
  authors:
    - StefanoBerlato
    - RobertoCarbone
    - AdamJLee
    - SilvioRanise
  abstract: >
    To facilitate the adoption of cloud by organizations, Cryptographic Access Control (CAC) is the obvious solution to control data sharing among users while preventing partially trusted Cloud Service Providers (CSP) to access sensitive data. Indeed, several CAC schemes have been proposed in the literature. Despite their differences, available solutions are based on a common set of entities—e.g., a data storage service or a proxy mediating the access of users to encrypted data—that operate in different (security) domains—e.g., on-premise or the CSP. However, the majority of the CAC schemes assumes a fixed assignment of entities to domains; this has security and usability implications that are not made explicit and can make inappropriate the use of a CAC scheme in certain scenarios with specific requirements. For instance, assuming that the proxy runs at the premises of the organization avoids the vendor lock-in effect but may substantially mine scalability. To the best of our knowledge, no previous work considers how to select the best possible architecture (i.e., the assignment of entities to domains) to deploy a CAC scheme for the requirements of a given scenario. In this paper, we propose a methodology to assist administrators to explore different architectures of CAC schemes for a given scenario. We do this by identifying the possible architectures underlying the CAC schemes available in the literature and formalize them in simple set theory. This allows us to reduce the problem of selecting the most suitable architecture satisfying a heterogeneous set of requirements arising from the considered scenario to a Multi-Objective Optimization Problem (MOOP) for which state-of-the-art solvers can be invoked. Finally, we show how the capability of solving the MOOP can be used to build a prototype tool assisting administrators to preliminary perform a ``What-if'' analysis to explore the trade-offs among the various architectures and then use available standards and tools (such as TOSCA and Cloudify) for automated deployment in multiple CSPs.
  destination: ASIACCS2020
  year: 2020
  doi: 10.1145/3320269.3384767
  urlComplementary: /complementary/ASIACCS2020
  urlNews: /news/2020/02/15/paper-accepted-at-asiaccs-2020/

- id: CODASPY2020_PN
  id_iris: 321325
  title: "The Good, the Bad and the (Not So) Ugly of Out-Of-Band Authentication with eID Cards and Push Notifications: Design, Formal and Risk Analysis"
  authors:
    - MarcoPernpruner
    - RobertoCarbone
    - SilvioRanise
    - GiadaSciarretta
  abstract: >
    Everyday life is permeated by new technologies allowing people to perform almost any kind of operation from their smart devices. Although this is amazing from a convenience perspective, it may result in several security issues concerning the need for authenticating users in a proper and secure way. Electronic identity cards (also called eID cards) play a very important role in this regard, due to the high level of assurance they provide in identification and authentication processes. However, authentication solutions relying on them are still uncommon and suffer from many usability limitations. In this paper, we thus present the design and implementation of a novel passwordless, multi-factor authentication protocol based on eID cards. To reduce known usability issues while keeping a high level of security, our protocol leverages push notifications and mobile devices equipped with NFC, which can be used to interact with eID cards. In addition, we evaluate the security of the protocol through a formal security analysis and a risk analysis, whose results emphasize the acceptable level of security.
  destination: CODASPY2020
  year: 2020
  doi: 10.1145/3374664.3375727
  urlComplementary: /complementary/CODASPY2020
  urlNews: /news/2019/12/01/paper-accepted-at-codaspy-2020/

- id: COSE2020_MFA
  title: "A Survey on Multi-Factor Authentication for Online Banking in the Wild"
  authors:
    - FedericoSinigaglia
    - RobertoCarbone
    - GabrieleCosta
    - NicolaZannone
  abstract: >
    In recent years, the usage of online banking services has considerably increased. To protect the sensitive resources managed by these services against attackers, banks have started adopting Multi-Factor Authentication (MFA). To date, a variety of MFA solutions have been implemented by banks, leveraging different designs and features and providing a non-homogeneous level of security and user experience. Public and private authorities have defined laws and guidelines to guide the design of more secure and usable MFA solutions, but their influence on existing MFA implementations remains unclear. In this work, we present a latitudinal study on the adoption of MFA and the design choices made by banks operating in different countries. In particular, we evaluate the MFA solutions currently adopted in the banking sector in terms of (i) compliance with laws and best practices, (ii) robustness against attacks and (iii) complexity. We also investigate possible correlations between these criteria. Based on this study, we identify a number of lessons learned and open challenges.
  destination: COSE
  year: 2020
  doi: 10.1016/j.cose.2020.101745
  urlComplementary: https://mfa-team.github.io/
  urlNews: /news/2020/02/02/paper-accepted-at-cose/

- id: CPS4CIP2020_TLS
  id_iris: 324801
  title: "TLSAssistant goes FINSEC: A Security Platform Integration Extending Threat Intelligence Language "
  authors:
    - SalvatoreManfredi
    - SilvioRanise
    - GiadaSciarretta
    - AlessandroTomasi
  abstract: >
    We present the integration of TLSAssistant, a tool for TLS vulnerability scanning and mitigation, with an online platform of services for cybersecurity in critical infrastructure. We highlight the added value of intelligence sharing and synergies with other services on the platform, as well as the non-trivial challenges encountered in the process.
  destination: CPS4CIP2020
  year: 2020

- id: DETIPS2020
  id_iris: 324206
  title: "Verifiable Contracting: A Use Case for Onboarding and Contract Offering in Financial Services with eIDAS and Verifiable Credentials"
  authors:
    - SergioManuelNobregaGoncalves
    - AlessandroTomasi
    - AndreaBisegna
    - GiulioPellizzari
    - SilvioRanise
  destination: DETIPS2020
  abstract: >
    We investigate the combined use of eIDAS-based electronic identity and Verifiable Credentials for remote onboarding and contracting, and provide a proof-of-concept implementation based on SAML authentication. The main non-trivial value derived from this proposal is a higher degree of assurance in the contract offering phase for the Contracting Service Provider.
  year: 2020
  doi: 10.1007/978-3-030-66504-3_8 

- id: ETAA2020_MIG
  id_iris: 325778
  title: "Micro-Id-Gym: a Flexible Tool for Pentesting Identity Management Protocols in the Wild and in the Laboratory"
  authors:
    - AndreaBisegna
    - RobertoCarbone
    - GiulioPellizzari
    - SilvioRanise
  abstract: >
    Identity Management (IdM) solutions are increasingly important for digital infrastructures of both enterprises and public administrations. Their security is a mandatory pre-requisite for building trust in current and future digital ecosystems. Unfortunately, not only their secure deployment but even their usage are non-trivial activities that require a good level of security awareness. In order to test whether known exploits can be reproduced in different environments, better understand their effects and facilitate the discovery of new vulnerabilities, we need to have a reliable testbed. For this, we present Micro-Id-Gym which abstractly supports two main activities: the creation of sandboxes with an IdM protocol deployment and the pentesting of IdM protocol deployments in the wild or in the laboratory (on the created sandboxes).
  destination: ETAA2020
  year: 2020
  doi: 10.1007/978-3-030-64455-0_5

- id: ETAA2020_OIDC
  id_iris: 324008
  title: Automated and Secure Integration of the OpenID Connect iGov Profile in Mobile Native Applications
  authors:
    - AmirSharif
    - RobertoCarbone
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    Electronic identification schemes have been built to simplify citizens access to online public administration services and reduce password fatigue via a single sign-on experience. To provide a precise specification for government and public service domains on how to protect the user’s identity information and activity from unintentional exposure, the OAuth working group together with the OpenID Connect foundation have published the International Government Assurance Profile (iGov) document. As the specification contains high-level concepts and brings together a lot of insights from already published documents to increase the baseline security and structure deployments, it may be unclear or misleading for mobile application developers. This is mainly due to the fact that firstly, they are not usually security experts and secondly, the aforementioned documents are not mostly designed for the native applications that can affect the implementation security based on the differences between the native and web environment. The aforementioned source of uncertainty for inexperienced developers can lead to various threats that can expose user’s resources. To avoid these problems, we demystify the iGov profile for non-security experts by extracting the wealth information from the iGov specifications, and we apply the best current practices for native applications within the iGov profile to conceptualize the flow for native applications. Furthermore, we provide a wizard-based approach to automatically integrate the secure code for the iGov profile in Android native applications.
  destination: ETAA2020
  year: 2020
  doi: 10.1007/978-3-030-64455-0_4
  urlComplementary: /complementary/ETAA2020_OIDC

- id: ICTSecMag202006_TLSA
  title: "TLSAssistant: uno strumento per mitigare i problemi di sicurezza di TLS"
  authors:
    - SalvatoreManfredi
    - SilvioRanise
    - GiadaSciarretta
  destination: ICTSecurityMagazine
  year: 2020
  url: https://www.ictsecuritymagazine.com/articoli/tlsassistant-uno-strumento-per-mitigare-i-problemi-di-sicurezza-di-tls/
  urlNews: /news/2020/06/03/article-published-on-ict-security-magazine/

- id: ITASEC2020_OIC
  title: Automated Secure Code Generation for OpenID Connect iGov Profile in Mobile Native Applications
  authors:
    - AmirSharif
    - RobertoCarbone
    - SilvioRanise
    - GiadaSciarretta
  destination: ITASEC2020
  year: 2020
  urlNews: /news/2020/01/07/papers-accepted-at-itasec-2020/

- id: ITASEC2020_PP
  title: "Pull Printing with National eID Cards: An Open-source and Software-oriented Implementation"
  authors:
    - MatteoLeonelli
    - UmbertoMorelli
    - SilvioRanise
    - GiadaSciarretta
  abstract: >
    Pull printing is the set of technologies and processes that allow print jobs to be released according to specific conditions; typically user authentication and proximity to a printer. In this paper, we propose an open-source and software-oriented pull printing infrastructure that use a cloud print orchestrator and leverages the OpenID Connect protocol and the Italian electronic identity card to protect user prints with a second-factor authentication. Our goal is to prevent print-related data breaches and tackle the challenges that hinder the widespread adoption of more secure printing solutions: costs and user experience.
  destination: ITASEC2020
  year: 2020
  urlNews: /news/2020/01/07/papers-accepted-at-itasec-2020/
  
- id: JISA2020
  id_iris: 321185
  title: A Large-Scale Study on the Adoption of Anti-Debugging and Anti-Tampering Protections in Android Apps
  authors:
    - StefanoBerlato
    - MarianoCeccato
  abstract: >
    Android apps are subject to malicious reverse engineering and code tampering for many reasons, like premium features unlocking and malware piggybacking. Scientific literature and practitioners proposed several Anti-Debugging and Anti-Tampering protections, readily implementable by app developers, to empower Android apps to react against malicious reverse engineering actively. However, the extent to which Android app developers deploy these protections is not known. In this paper, we describe a large-scale study on Android apps to quantify the practical adoption of Anti-Debugging and Anti-Tampering protections. We analyzed 14,173 apps from 2015 and 23,610 apps from 2019 from the Google Play Store. Our analysis shows that 59% of these apps implement neither Anti-Debugging nor Anti-Tampering protections. Moreover, half of the remaining apps deploy only one protection, not exploiting the variety of available protections. We also observe that app developers prefer Java to Native protections by a ratio of 99 to 1. Finally, we note that apps in 2019 employ more protections against reverse engineering than apps in 2015.
  destination: JISA
  year: 2020
  doi: 10.1016/j.jisa.2020.102463
  urlNews: /news/2020/01/29/paper-accepted-at-jisa/

- id: SACMAT2020
  id_iris: 325002
  title: "Deploying Access Control Enforcement for IoT in the Cloud-Edge Continuum with the help of the CAP Theorem"
  authors:
    - TahirAhmad
    - UmbertoMorelli
    - SilvioRanise
  abstract: >
    The CAP Theorem is used by distributed system practitioners to investigate the necessary trade-offs in the design and development of distributed systems, mainly databases and web applications. In this paper, we use it to reason about access control systems designed for the Internet of Things (IoT). 
    We validate our approach by experimentally investigating alternative architectural designs to enforce access control in a smart lock system using the cloud-edge IoT platform offered by Amazon. 
    We discuss the trade-off between security and performance that may help IoT designers choose the most suitable architecture supporting their requirements.
  destination: SACMAT2020
  year: 2020
  urlNews: /news/2020/04/08/paper-accepted-at-sacmat-2020/

- id: SecAssAPIFinancial_book_2020
  id_iris: 325801
  title: "Automated Assistance to the Security Assessment of API for Financial Services in book Cyber-Physical Threat Intelligence for Critical Infrastructures Security: A Guide to Integrated Cyber-Physical Protection of Modern Critical Infrastructures"
  authors:
    - AndreaBisegna
    - RobertoCarbone
    - MarianoCeccato
    - SalvatoreManfredi
    - SilvioRanise
    - GiadaSciarretta
    - AlessandroTomasi
    - EmanueleViglianisi
  year: 2020
  destination: SecAssAPIFinancial_book_2020
  doi: 10.1561/9781680836875

- id: SECRYPT2020
  id_iris: 322586
  title: "Multi-Stakeholder Cybersecurity Risk Assessment for Data Protection"
  authors:
    - MajidMollaeefar
    - AlbertoSiena
    - SilvioRanise
  abstract: >
    To ensure the effectiveness of the adopted security measures and minimize the impact of security issues on the rights and freedom of individuals, the General Data Protection Regulation (GDPR) requires to carry out a Data Processing Impact Assessment (DPIA). Such an assessment differs from traditional risk analyses in which the actor carrying out the evaluation is also the one interested in reducing its risk. Conflicts may thus arise between the need of protecting data subjects rights and organizations that shall provide adequate security measures while struggling with various types of constraints (e.g., budget). To alleviate this problem, we introduce the Multi-Stakeholder Risk Trade-off Analysis Problem, (MSRToAP) and propose an automated technique to solve their instances. We then show how this can help data controllers make more informed decisions about which security mechanisms allow for a better trade-off between their requirements and those of the data subjects. For concreteness, we illustrate the proposed on a simple yet realistic use case scenario.
  destination: SECRYPT2020
  year: 2020
  doi: 10.5220/0009822703490356

- id: TIFS2020
  id_iris: 325070
  title: "SARA: Secure Asynchronous Remote Attestation for IoT Systems"
  authors:
    - EdliraDushku
    - MdMasoomRabbani
    - MauroConti
    - LuigiMancini
    - SilvioRanise
  abstract: >
    Remote attestation has emerged as a valuable security mechanism which aims to verify remotely whether or not a potentially untrusted device has been compromised. The protocols of Remote attestation are particularly important for securing Internet of Things (IoT) systems which, due to the large number of interconnected devices and limited security protections, are susceptible to a wide variety of cyber attacks. To guarantee the integrity of a software running on a single device, remote attestation is usually executed as an uninterrupted procedure: at the attestation time, a device stops the normal operation and executes the attestation of the entire device without interruption. The remote attestation protocols that aim to attest a large number of devices also follow the assumption on uninterrupted execution: when a device attests its network neighbours, each device verified in the neighborhood suspends its normal operation until the attestation protocol is completed. To avoid unnecessary suspension of the normal operation of the devices, this paper proposes a novel Secure Asynchronous Remote Attestation (SARA) protocol that releases the constraint of synchronous interaction among devices. In particular, SARA is an attestation protocol that exploits asynchronous communication capabilities among IoT devices in order to attest a distributed IoT service executed by them. SARA verifies both that each IoT device is not compromised (device trustworthiness), and that the exchanged communication data have not maliciously influence the communicating devices (legitimate operations). By tracing the execution order of each service invocation of an asynchronous distributed service, SARA allows each service to collect accurately historical data of its interactions, and transmits asynchronously such historical data to other interacting services. We have implemented and validated SARA through a realistic simulation on the Contiki emulator that demonstrates the functionality and efficiency of our protocol. The results confirm the suitability of SARA for low-end devices.
  destination: TIFS
  year: 2020
  doi: 10.1109/TIFS.2020.2983282

- id: TOPS2020
  id_iris: 325068
  title: Formal Analysis of Mobile Multi-Factor Authentication with Single Sign-On Login
  authors:
    - RobertoCarbone
    - SilvioRanise
    - GiadaSciarretta
    - LucaViganò
  abstract: >
    Over the last few years, there has been an almost exponential increase in the number of mobile applications that deal with sensitive data, such as applications for e-commerce or health. When dealing with sensitive data, classical authentication solutions based on username-password pairs are not enough, and multi-factor authentication solutions that combine two or more authentication factors of different categories are required instead. Even if several solutions are currently used, their security analyses have been performed informally or semi-formally at best, and without a reference model and a precise definition of the multi-factor authentication property. This makes a comparison among the different solutions both complex and potentially misleading. In this paper, we first present the design of two reference models for native applications based on the requirements of two real-world use-case scenarios. Common features between them are the use of one-time password approaches and the support of a single sign-on experience. Then, we provide a formal specification of our threat model and the security goals, and discuss the automated security analysis that we performed. Our formal analysis validates the security goals of the two reference models we propose and provides an important building block for the formal analysis of different multi-factor authentication solutions.
  destination: TOPS
  year: 2020
  doi: 10.1145/3386685
  urlComplementary: /complementary/TOPS2020
  urlNews: /news/2020/03/12/paper-accepted-at-tops/

- id: TOPS2020_2
  id_iris: 329068
  title: "Formal Modelling and Automated Trade-Off Analysis of Enforcement Architectures for Cryptographic Access Control in the Cloud"
  authors:
    - StefanoBerlato
    - RobertoCarbone
    - AdamJLee
    - SilvioRanise
  abstract: >
    To facilitate the adoption of cloud by organizations, Cryptographic Access Control (CAC) is the obvious solution to control data sharing among users while preventing partially trusted Cloud Service Providers (CSP) from accessing sensitive data. Indeed, several CAC schemes have been proposed in the literature. Despite their differences, available solutions are based on a common set of entities---e.g., a data storage service or a proxy mediating the access of users to encrypted data---that operate in different (security) domains---e.g., on-premise or the CSP. However, the majority of these CAC schemes assumes a fixed assignment of entities to domains; this has security and usability implications that are not made explicit and can make inappropriate the use of a CAC scheme in certain scenarios with specific trust assumptions and requirements. For instance, assuming that the proxy runs at the premises of the organization avoids the vendor lock-in effect but may give rise to other security concerns (e.g., malicious insiders attackers). To the best of our knowledge, no previous work considers how to select the best possible architecture (i.e., the assignment of entities to domains) to deploy a CAC scheme for the trust assumptions and requirements of a given scenario. In this paper, we propose a methodology to assist administrators in exploring different architectures for the enforcement of CAC schemes in a given scenario. We do this by identifying the possible architectures underlying the CAC schemes available in the literature and formalizing them in simple set theory. This allows us to reduce the problem of selecting the most suitable architectures satisfying a heterogeneous set of trust assumptions and requirements arising from the considered scenario to a decidable Multi-Objective Combinatorial Optimization Problem (MOCOP) for which state-of-the-art solvers can be invoked. Finally, we show how we use the capability of solving the MOCOP to build a prototype tool assisting administrators to preliminary perform a ``What-if'' analysis to explore the trade-offs among the various architectures and then use available standards and tools (such as TOSCA and Cloudify) for automated deployment in multiple CSPs.
  destination: TOPS
  year: 2020
  urlComplementary: /complementary/TOPS2020_2
  
## 2021
- id: CODASPY2021_SPP
  id_iris: 331090
  title: "Secure Pull Printing with QR Codes and National eID Cards: A Software-oriented Design and an Open-source Implementation"
  authors:
    - MatteoLeonelli
    - UmbertoMorelli
    - SilvioRanise
    - GiadaSciarretta
  abstract: >
    With more systems becoming digitized, enterprises are adopting cloud technologies and outsourcing non-critical services to reduce the pressure on IT departments. In this process, it is crucial to achieving the right balance between costs, usability and security; prioritizing security over the rest when handling sensitive data. Considering the print management, often off-premise, many enterprises report at least one print-related security incident that led to data loss in the past year. This problem can damage the enterprise business, in particular considering the fines prescribed by current regulations or its reputation. Focusing on securing enterprise printing, pull printing is the set of technologies and processes that allow the release of print jobs according to specific conditions; typically user authentication and proximity to a printer. We design a software-oriented pull printing infrastructure that supports a print release mechanism using QR codes and electronic IDentity cards as a second-factor authenticator. Our solution addresses the costs, as any medium-size organization can adopt our open-source solution without additional devices or access badges; and the user experience, as we offer a driverless print environment and a user-friendly mobile application.
  destination: CODASPY2021
  year: 2021
  doi: 10.1145/3422337.3447847
  urlComplementary: /complementary/CODASPY2021
  urlNews: /news/2019/12/01/paper-accepted-at-codaspy-2021/

- id: DBSec2021
  id_iris: 327486
  title: "Automated Risk Assessment and What-if Analysis of OpenID Connect and OAuth 2.0 Deployments"
  authors:
    - SalimehDashti
    - AmirSharif
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    The introduction of the Payment Service Directive (PSD2) has accelerated financial services and open banking growth. Deploying appropriate identity management solutions is crucial. This implies the adoption of secure protocols for authentication and authorization, such as OpenID Connect and OAuth 2.0. The PSD2 also requires the application of the General Data Protection Regulation (GDPR) when transactions involve personal data. In turn, the GDPR mandates a Data Protection Impact Assessment (DPIA) for assessing risks posed to data subjects’ rights and freedom. This is a time-consuming and challenging task requiring heterogeneous skills that include the knowledge of best practices for deploying protocols, security mechanisms adopted by available identity management providers, and the capability to perform careful what-if analysis of the possible alternatives. To assist users in this task, we propose a methodology based on the formalization of the what-if analysis as an optimization problem that available tools can solve.  The formalization is derived from the OAuth 2.0 and OpenID connects standards, security best practices to mitigate threats, and thorough the evaluation of 19 identity management providers to check their supported features concerning the identified set of features for OAuth/OIDC solutions. We apply the methodology to assist controllers and identify the most appropriate security setup to drive the process of making financial services compliant with the PSD2.
  destination: DBSec2021
  year: 2021
  urlNews: /news/2021/06/04/paper-accepted-at-dbsec-2021/

- id: ETAA2021_MIG
  id_iris: 331569
  title: "Integrating a Pentesting Tool for IdM Protocols in a Continuous Delivery Pipeline"
  authors:
    - AndreaBisegna
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    Identity Management (IdM) solutions are increasingly important for digital infrastructures of both enterprises and public administrations. Their security is a mandatory prerequisite for building trust in current and future digital ecosystems. IdM solutions are usually large-scale complex software systems maintained and developed by several groups of ICT professionals. Continuous Delivery (CD) pipeline is adopted to make maintenance, extension, and deployment of such solutions as efficient and repeatable as possible. For security, CD pipeline is also used as a continuous risk assessment to quickly evaluate the security impact of changes. Several tools have been developed and integrated in the CD pipeline to support this view in the so called DevSecOps approach with the notable exception of a tool for protocol pentesting and compliance against standards such as SAML 2.0, OAuth 2.0 and OpenID Connect. To fill this gap, we propose an approach to integrate Micro-Id-Gym—a tool for the automated pentesting of IdM deployments—in a CD pipeline. We report our experience in doing this and discuss the advantages of using the tool in the context of a joint effort with Poligrafico e Zecca dello Stato Italiano to build a digital identity infrastructure.
  destination: ETAA2021
  year: 2021
  doi: 10.1007/978-3-030-93747-8_7

- id: ETACS2021
  id_iris: 331068
  title: "Do Security Reports Meet Usability? - Lessons Learned from Using Actionable Mitigations for Patching TLS Misconfigurations"
  authors:
    - SalvatoreManfredi
    - MarianoCeccato
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    Several automated tools have been proposed to detect vulnerabilities. These tools are mainly evaluated in terms of their accuracy in detecting vulnerabilities, but the evaluation of their usability is a commonly neglected topic. Usability of automated security tools is particularly crucial when dealing with problems of cryptographic protocols for which even small—apparently insignificant—changes in their configuration can result in vulnerabilities that, if exploited, pave the way to attacks with dramatic consequences for the confidentiality and integrity of exchanged messages. This becomes even more acute when considering such ubiquitous protocols as the one for Transport Layer Security (TLS for short). In this paper, we present the design and the lessons learned of a user study, meant to compare two different approaches when reporting misconfigurations. Results reveal that including contextualized actionable mitigations in security reports significantly impact the accuracy and the time needed to patch TLS vulnerabilities. Along with the lessons learned, we share the experimental material that can be used during cybersecurity labs to let students configure and patch TLS first-hand.
  destination: ETACS2021
  year: 2021
  urlComplementary: /complementary/ETACS2021
  urlNews: /news/2021/05/31/paper-accepted-at-etacs-2021
  doi: 10.1145/3465481.3469187

- id: ICSE2021
  id_iris: 324116
  title: Security Analysis of Permission Re-delegation Vulnerabilities in Android Apps
  authors:
    - BiniamFissehaDemissie
    - MarianoCeccato
    - LwinKhinShar
  abstract: >
    The Android platform facilitates reuse of app functionalities by allowing an app to request an action from another app through inter-process communication mechanism. This feature is one of the reasons for the popularity of Android, but it also poses security risks to end users because malicious, unprivileged apps could exploit this feature to make privileged apps perform privileged actions on behalf of them.
    In our journal paper, we investigate the hybrid use of program analysis, genetic algorithm based test generation, natural language processing, machine learning techniques for precise detection of permission re-delegation vulnerabilities in Android apps. Our approach first groups a large set of benign and ”safe” apps into different clusters, based on their similarities in terms of functional descriptions. It then generates permission re-delegation model for each cluster, which characterizes common permission re-delegation behaviors of the apps in the cluster. Given an app under test, our approach checks whether it has permission re-delegation behaviors that deviate from the model of the cluster it belongs to. If that is the case, it generates test cases to detect the vulnerabilities. We evaluated the vulnerability detection capability of our approach based on 1,258 official apps and 20 mutated apps. Our approach achieved 81.8% recall and 100% precision. We also compared our approach with two static analysis-based approaches — Covert and IccTA — based on 595 open source apps. Our approach detected 30 vulnerable apps whereas Covert detected one of them and IccTA did not detect any. Executable proof-of-concept attacks generated by our approach were reported to the corresponding app developers.
  destination: ICSE2021
  year: 2021
  urlNews: /news/2021/05/23/paper-accepted-at-icse-2021/

- id: IJIS2021
  id_iris: 331088
  title: "Extending access control in AWS IoT through event-driven functions: an experimental evaluation using a smart lock system"
  authors:
    - TahirAhmad
    - UmbertoMorelli
    - SilvioRanise
    - NicolaZannone
  abstract: >
    In recent years, the design of effective authorization mechanisms for IoT and, in particular, for smart home applications has gained increasing attention from researchers and practitioners. However, very little attention is given to the performance evaluation of those authorization mechanisms. To fill this gap, this paper presents a thorough experimental evaluation of cloud- and edge-based access control mechanisms for smart home applications. We discuss the main architectural choices, namely (a) where the access control logic is deployed (in the cloud or the edge) and (b) how the attributes needed for policy evaluation are provided to the policy evaluation point and identify possible deployment models for cloud- and edge-based access control mechanisms. To study the impact of these choices on the performance of smart homes, we realized the identified deployment models within the IoT platforms offered by Amazon Web Services (AWS), namely AWS IoT and Greengrass, and empirically evaluate them using a smart lock system. Based on our experimental evaluation, we provide recommendations to both researchers and practitioners.
  destination: IJIS
  year: 2021
  doi: 10.1007/s10207-021-00558-3
  
- id: IOTSECFOR2021
  id_iris: 331086
  title: "DoS Attacks in Available MQTT Implementations: Investigating the Impact on Brokers and Devices, and supported Anti-DoS Protections."
  authors:
    - UmbertoMorelli
    - IvanVaccari
    - SilvioRanise
    - EnricoCambiaso
  abstract: >
    The Internet of Things is a widely adopted and pervasive technology, but also one of the most conveniently attacked given the volume of shared data and the availability of affordable but insecure products. This paper investigates two classes of denial of service (DoS) attacks that target the handling of message queues in MQTT, one of the most broadly used IoT protocols. The first attack attempts to saturate the MQTT broker resources, while the second exploits the broker to perform an amplification attack against the connected clients. We demonstrate the effectiveness of the attacks and indicate the parameters that would hinder the capabilities of a DoS attacker in three open-source MQTT implementations: Mosquitto, VerneMQ and EMQ X. To improve the security awareness in MQTT-based deployments, we integrate the attacks and mitigations in MQTTSA, a tool that detects MQTT misconfigurations and provides security-oriented recommendations and configuration snippets.
  destination: IOTSECFOR2021
  year: 2021
  urlComplementary: /complementary/IOTSECFOR2021
  urlNews: /news/2021/06/05/paper-accepted-at-IoT-SECFOR-2021/

- id: JISA2021
  id_iris: 329426
  title: "Best Current Practices for OAuth/OIDC Native Apps: A Study of their Adoption in Popular Providers and Top-Ranked Android Clients"
  authors:
    - AmirSharif
    - RobertoCarbone
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    OAuth 2.0 and OpenID Connect have been extensively integrated into mobile applications during recent years to manage access delegation and reduce password fatigue via a single sign-on experience. To provide a precise specification for mobile application developers on how to secure their implementations, the OAuth Working Group has published a set of best current practices called “OAuth 2.0 for Native Apps”. Nevertheless, many available mobile applications still suffer from poor implementations leading to serious security issues. To find the source of the problem, we perform a comprehensive analysis on 14 popular OAuth 2.0 and OpenID Connect providers and 87 top-ranked Google Play Store applications selected out of 2505 top-ranked applications to investigate their compliance with the best current practices for native apps. Our analysis reveals that only 7 OAuth 2.0 and OpenID Connect providers and 5 Google Play Store applications are fully compliant with the best current practices. To help mobile application developers with securing the implementation of OAuth 2.0 and OpenID Connect solutions, we introduce a wizard-based approach to assist mobile application developers to integrate multiple third-party OAuth 2.0 and OpenID Connect providers in their mobile applications. To verify the correctness and security of the integrated code by our wizard-based approach, we performed a security analysis by using both open-source and commercial source-code analysis tools. The result of security analysis confirms the security of using our approach in mobile applications, even though it raises some security issues related to the general implementation of mo- bile applications (e.g., insufficient code obfuscation). Despite these issues are out of the scope of our work, they stimulate interesting challenges at the intersection of theory and practice of security in mobile applications using OAuth 2.0 and OpenID Connect.
  destination: JISA
  year: 2021
  urlNews: /news/2021/12/14/paper-accepted-at-jisa-2021/
  doi: 10.1016/j.jisa.2021.103097

- id: SECRYPT2021
  id_iris: 327626
  title: "A Framework for Security and Risk Analysis of Enrollment Procedures: Application to Fully-Remote Solutions Based on eDocuments"
  authors:
    - MarcoPernpruner
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    More and more online services are characterised by the need for strongly verifying the real-world identity of end users, especially when sensitive operations have to be carried out: just imagine a fully-remote signature of a contract, and what could happen whether someone managed to perform it by using another person's name. For this reason, the identity management lifecycle contains specific procedures – called enrollment or onboarding – providing a certain level of assurance on digital users' real identities. These procedures must be as secure as possible to prevent frauds and identity thefts. In this paper, we present a framework composed of a specification language, a security analysis methodology and a risk analysis methodology for enrollment solutions. For concreteness, we apply our framework to a real use case (i.e., fully-remote solutions relying on electronic documents as identity evidence) in the context of a collaboration with an Italian FinTech startup. Beyond validating the framework, we analyse and highlight the essential role of mitigations on the overall security of enrollment procedures.
  destination: SECRYPT2021
  year: 2021
  urlComplementary: /complementary/SECRYPT2021
  urlNews: 
  doi: 10.5220/0010554502220233

- id: SECRYPT2021_2
  id_iris: 327652
  title: "Cryptographic Enforcement of Access Control Policies in the Cloud: Implementation and Experimental Assessment"
  authors:
    - StefanoBerlato
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    While organisations move their infrastructure to the cloud, honest but curious Cloud Service Providers (CSPs) threaten the confidentiality of cloud-hosted data. In this context, many researchers proposed Cryptographic Access Control (CAC) schemes to support data sharing among users while preventing CSPs from accessing sensitive data. However, the majority of these schemes focuses on high-level features only and cannot adapt to the multiple requirements arising in different scenarios. Moreover, (almost) no CAC scheme implementation is available for enforcement of authorisation policies in the cloud, and performance evaluation is often over- looked. To fill this gap, we propose the toolchain COERCIVE, short for CryptOgraphy killEd (the honest but) cuRious Cloud servIce proVidEr, which is composed of two tools: TradeOffBoard and CryptoAC. TradeOff- Board assists organisations in identifying the optimal CAC architecture for their scenario. CryptoAC enforces authorisation policies in the cloud by deploying the architecture selected with TradeOffBoard. In this paper, we describe the implementation of CryptoAC and conduct a thorough performance evaluation to demonstrate its scalability and efficiency with synthetic benchmarks.
  destination: SECRYPT2021
  year: 2021
  urlComplementary: /complementary/SECRYPT2021_2
  urlNews: /news/2021/05/17/paper-accepted-at-secrypt-2021/
  
- id: SMDS2021
  id_iris: 328826
  title: "Assessing the Effectiveness of the Shared Responsibility Model for Cloud Databases: the Case of Google's Firebase"
  authors:
    - BiniamFissehaDemissie
    - SilvioRanise
  abstract: >
    Migrating databases to the cloud requires the adoption of the shared responsibility model for protecting data. The database-as-a-service provider secures the database from different kinds of attacks while the developer defines the access control policy to prevent unauthorized access. Recent reports show that developers fail to properly secure their cloud databases leading to sensitive data leaks. In this paper, we investigate the prevalence of the access control misconfigurations in 50K+ top Android apps that use one of the most popular cloud database services, namely Firebase. Overall, we found 763 apps (1 billion downloads) with public databases and 536 apps (630 million downloads) with world-writable databases. Considering the popularity of these apps and the cross-platform nature of Firebase databases, our findings reveal a worrying state in the adoption of the shared responsibility model for the security of cloud databases. To assist developers, we make our prototype tool publicly available as an Android Studio plugin. The plugin performs static analysis to automatically extract Firebase database information from the app under development and checks its configuration status.
  destination: SMDS2021
  year: 2021
  urlNews: /news/2021/06/05/paper-accepted-at-IoT-SECFOR-2021/

- id: SMDS2021_Blockchain
  id_iris: 328846
  title: Blockchain Based RAN Data Sharing
  authors:
    - AndreasHeiderAviet
    - DannyRoswinOllik
    - StefanoBerlato
    - SilvioRanise
    - RobertoCarbone
    - VanThanhLe
    - NabilElIoini
    - ClausPahl
    - HamidBerzegar
  abstract: >
    Providing seamless connectivity and services across national borders are intricate challenges with multifarious underlying aspects, ranging from the network management to business and political considerations. Since the cross-border inter-Public Land Mobile Network (PLMN) network handover is currently not available in European cellular networks, we present a complementary approach, diminishing the connectivity gap to a minimum. By leveraging Distributed Ledger Technology (DLT), we establish a dynamic, secure data exchange and management solution between several Mobile Network Operators (MNOs) of different countries. Systematically integrating foreign cell and base station parameter (i.e., Radio Access Network (RAN) data) of border regions into the internal network management systems permits their usage in standardized Mobility Management procedures. We demonstrate that this type of collaboration on the interMNO network governance considerably improves the network quality and customer experience when crossing national borders. Since foreign RAN data is also required for the inter-PLMN network handover (and can serve many additional purposes) and provided that our solution is not relying on any specific mobile network technology generation (e.g., 4G or 5G), we conclude that it is a fundamental step towards an inter-MNO ecosystem beyond 5G.
  destination: SMDS2021
  year: 2021
  doi: 10.1109/SMDS53860.2021.00029

- id: T-ITS2021
  id_iris: 328626
  title: "Smart Card-Based Identity Management Protocols for V2V and V2I Communications in CCAM: a Systematic Literature Review"
  authors:
    - StefanoBerlato
    - MarcoCentenaro
    - SilvioRanise
  abstract: >
    Besides developing new Cooperative, Connected and Automated Mobility (CCAM) services for the improvement of road safety and travel experience, researchers are considering protection mechanisms to ensure the security of these services and the safety of involved users (drivers but also, e.g., cyclists and pedestrians). In particular, several Identity Management (IDM) protocols have been designed as the first line of defence against external attackers. Among these protocols, a promising trend in research consists in the use of a Smart Card (SC) as a technical enabler for strong authentication. Indeed, many SC-based IDM protocols for Vehicle-to-Vehicle (V2V) and Vehicle-to-Infrastructure (V2I) communications in real-time CCAM services have been proposed in the literature which present interesting features and promising usability experimental results. However, this research line is far from being exhausted, especially considering the recent spread of SC technologies and use cases. For this reason, in this paper we propose a systematic literature review on SC-based IDM protocols for real-time CCAM services. In particular, we identify characterising assumptions of CCAM scenarios and extrapolate a unified high-level view of the steps composing a SC-based IDM protocol. Then, we present a detailed survey of several SC-based IDM protocols. Finally, we identify trends in research and formulate guidelines and useful recommendations to provide a solid base which researchers can use as a starting point for the design of new and improved SC-based IDM protocols for CCAM scenarios.
  destination: T-ITS
  year: 2021
  doi: 10.1109/TITS.2021.3118721
  urlNews: /news/2021/10/26/paper-accepted-at-t-its/

- id: VTM2021
  id_iris: 328346
  title: "Safety-Related Cooperative, Connected, and Automated Mobility Services: Interplay Between Functional and Security Requirements"
  authors:
    - MarcoCentenaro
    - StefanoBerlato
    - RobertoCarbone
    - GianfrancoBurzio
    - GiuseppeFarandaCordella
    - RobertoRiggio
    - SilvioRanise
  abstract: >
    Together with the electrification of vehicles, the provision of cooperative, connected, and automated mobility (CCAM) services is a prominent recent trend in the automotive sector. Upcoming car models will be able to exchange messages between themselves and with road traffic authorities by means of vehicle-to-everything (V2X) communication—in particular, leveraging mobile network technologies for the cellular V2X (C-V2X) paradigm [1] . Moreover, (part of) such exchanged messages will be processed as a whole in, e.g., edge computing servers, to generate a global vision of the state of a given stretch of road. CCAM services will exploit vehicular information transport and processing to implement complex maneuvers in a (semi)automatic manner by interacting with the in-car network.
  destination: VTMagazine
  destinationAddon: Volume 16, Issue 4, December 2021, Pages 78-88
  year: 2021
  doi: 10.1109/MVT.2021.3089144
  
## 2022
- id: CODASPY2022_TLSA2
  id_iris: 332247
  title: "A Modular and Extensible Framework for Securing TLS"
  authors:
    - MatteoRizzi
    - SalvatoreManfredi
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    While being both extremely powerful and popular, TLS is a protocol that is hard to securely deploy. On the one hand, system administrators are required to grasp several security concepts to fully understand the impact of each option and avoid misconfigurations. 
    On the other hand, app developers should use cryptographic libraries in a secure way avoiding dangerous default settings or other subtleties (e.g., padding or modes of operations).
    To help secure TLS, we propose a modular framework, extensible with new features and capable of streamlining the mitigation process of known and newly discovered TLS attacks even for non-expert users.
  destination: CODASPY2022
  year: 2022
  doi: 10.1145/3508398.3511505
  urlNews: /news/2021/12/21/paper-accepted-at-codaspy-2022/
  
- id: DBSEC2022
  id_iris: 335865
  title: "End-to-End Protection of IoT Communications Through Cryptographic Enforcement of Access Control Policies"
  authors:
    - StefanoBerlato
    - RobertoCarbone
    - UmbertoMorelli
    - SilvioRanise
  abstract: >
    It is crucial to ensure the security and privacy of communications in IoT scenarios that process an increasingly large amount of sensitive data. In this context, we propose a cryptographic enforcement mechanism of access control policies to guarantee the confidentiality and integrity of messages exchanged with the MQTT protocol in presence of external attackers, malicious insiders and "honest-but-curious" service providers. A preliminary performance evaluation with a prototype implementation in an open-source tool shows the overhead is acceptable in relevant use case scenarios and provides a higher level of security with respect to other approaches.
  destination: DBSEC2022
  year: 2022
  doi: 10.1007/978-3-031-10684-2_14
  urlComplementary: /complementary/DBSEC2022
  
- id: EVOTEID2022
  title: "Adaptation of an i-voting scheme to Italian Elections for Citizens Abroad"
  authors:
    - RiccardoLongo
    - UmbertoMorelli
    - ChiaraSpadafora
    - AlessandroTomasi
  abstract: >
    We adapt the Araújo-Traoré protocol to Italian elections, with emphasis on anti-coercion measures. In this short paper we focus on a new method for managing anti-coercion credentials for each voter.
  destination: EVOTEID2022
  year: 2022
  doi: 10.15157/diss/027
  
- id: FARES2022_EIDAS
  id_iris: 333210
  title: "SoK: A Survey on Technological Trends for (pre)Notified eIDAS Electronic Identity Schemes"
  authors:
    - AmirSharif
    - MatteoRanzi
    - RobertoCarbone
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    The eIDAS Regulation aims to provide an interoperable European framework to enable EU citizens to authenticate and communicate with services of other Member States by using their national electronic identity. While a set of high-level requirements (e.g., related to privacy and security) are established to make interoperability among Member States possible, the eIDAS Regulation does not explicitly specify the technologies that can be adopted during the development phase to meet the requirements as mentioned earlier. This paper considers the technological trends of (pre)notified eIDAS electronic identity schemes used by Member States, and they satisfy the eIDAS regulation requirements. We do this by defining a set of research questions that allow us to investigate the correlations between different design dimensions such as security, privacy, and usability. Based on these findings, we provide a set of lessons learned that can be used by the security community to protect interoperable national digital identities more efficiently.
  destination: FARES2022
  awards: Best paper award
  year: 2022
  urlNews: /news/2022/06/10/papers-accepted-at-fares-2022/
  doi: 10.1145/3538969.3543817
  urlComplementary: /complementary/FARES2022_2
  
- id: FARES2022_ITS
  id_iris: 333787
  title: "Distributed Enforcement of Access Control policies in Intelligent Transportation System (ITS) for Situation Awareness"
  authors:
    - TahirAhmad
    - UmbertoMorelli
    - SilvioRanise
  abstract: >
    Intelligent Transport Systems (ITS) are crucial to support Situation Awareness (SA), which aims to keep a safe and efficient driving experience. While promising, ITS use for SA brings several security challenges, including enforcing access control policies in distributed environments with stringent computational constraints in terms of availability, consistency, and latency. Consequently, traditional mechanisms used to enforce authorization policies cannot be reused off-the-shelf but need to be carefully adapted to the particular requirements and minimize the overhead of access control enforcement. In this paper, we propose a distributed architecture for access control enforcement for ITS capable of satisfying the requirements of SA scenarios based on the idea of dynamically compiling a high-level specification of access control policies (written in the Attribute-Based Access Control model) into a set of low-level Access Control Lists that are easier to enforce. We discuss how to realize it by reusing well-known techniques developed in the field of distributed systems. To evaluate the applicability of the proposed approach, we build a prototype that we use to conduct an experimental evaluation in the context of two practical use case scenarios.
  destination: FARES2022
  year: 2022
  doi: 10.1145/3538969.3543792
  urlNews: /news/2022/06/10/papers-accepted-at-fares-2022/

- id: JOWUA2022
  id_iris: 332248
  title: "Empirical Validation on the Usability of Security Reports for Patching TLS Misconfigurations: User- and Case-Studies on Actionable Mitigations"
  authors:
    - SalvatoreManfredi
    - MarianoCeccato
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    Several automated tools have been proposed to detect vulnerabilities. These tools are mainly evaluated in terms of their accuracy in detecting vulnerabilities, but the evaluation of their usability is commonly neglected. Usability of automated security tools is particularly crucial when dealing with problems of cryptographic protocols for which even small—apparently insignificant—changes in configuration can result in vulnerabilities that, if exploited, pave the way to attacks with dramatic consequences for the confidentiality and integrity of the exchanged messages. This becomes even more acute when considering such ubiquitous protocols as the one for Transport Layer Security (TLS for short). In this paper, we present the design and the lessons learned of a user study, meant to compare two different approaches when reporting misconfigurations. Results reveal that including contextualized actionable mitigations in security reports significantly impact the accuracy and the time needed to patch TLS vulnerabilities. We used these results to build an open-source tool called TLSAssistant, able to combine state-of-the-art analyzers with a report systems that generates actionable mitigations to assist the user. Finally, we report our experience in using TLSAssistant in two case studies conducted in a corporate environment.
  destination: JOWUA
  year: 2022
  doi: 10.1145/3508398.3511505

- id: MDPI2022
  id_iris: 335107
  title: "The eIDAS Regulation: A Survey of Technological Trends for European Electronic Identity Schemes"
  authors:
    - AmirSharif
    - MatteoRanzi
    - RobertoCarbone
    - GiadaSciarretta
    - FrancescoAntonioMarino
    - SilvioRanise
  abstract: >
    The eIDAS regulation aims to provide an interoperable European framework to enable EU citizens to authenticate and communicate with services of other Member States by using their national electronic identity. While a number of high-level requirements (e.g., related to privacy and security) are established to make interoperability among Member States possible, the eIDAS regulation does not explicitly specify the technologies that can be adopted during the development phase to meet the requirements as mentioned earlier. To the best of our knowledge, there is no work available in the literature investigating the technological trends within the notified eIDAS electronic identity schemes used by Member States. To fill this gap, this paper analyzes how the different technological trends of notified schemes satisfy the requirements of the eIDAS regulation. To do this, we define a set of research questions that allow us to investigate the correlations between different design dimensions such as security, privacy, and usability. Based on these findings, we provide a set of lessons learned that would be valuable to the security community, as they can provide useful insights on how to more efficiently protect interoperable national digital identities. Furthermore, we provide a brief overview regarding the new eIDAS regulation (eIDAS 2.0) that aims to provide a more privacy-preserving electronic identity solution by moving from a centralized approach to a decentralized one.
  destination: MDPI-applsci
  year: 2022
  urlNews: /news/2022/12/08/papers-accepted-at-MDPI-2022/
  doi: 10.3390/app122412679
  urlComplementary: /complementary/MDPI2022
    
- id: SACMAT2022_TLSA2
  id_iris: 332827
  title: "Demo: TLSAssistant v2 - A Modular and Extensible Framework for Securing TLS"
  authors:
    - MatteoRizzi
    - SalvatoreManfredi
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    To grasp the security implications of the various TLS configuration options, system administrators and app developers must be familiar with a wide range of concepts, including cryptography. To assist users in this task, we propose TLSAssistant - a modular and extensible framework designed to streamline the discovery and mitigation of potential vulnerabilities in TLS deployments. This demo will focus on two of the four available analysis types.
  destination: SACMAT2022
  year: 2022
  doi: 10.1145/3532105.3535042
  urlNews: /news/2022/04/25/demo-accepted-at-sacmat-2022/

## 2023
- id: ARES2023
  id_iris: 338827
  title: "Cross-Domain Sharing of User Claims: A Design Proposal for OpenID Connect Attribute Authorities"
  authors:
    - AmirSharif
    - FrancescoAntonioMarino
    - GiadaSciarretta
    - GiuseppeDeMarco
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    An Attribute Authority is an entity responsible for establishing, maintaining, and sharing a subject’s qualified attributes, such as titles and qualifications. In the OpenID Connect digital identity ecosystem, this entity is distinct from Identity Providers that manage only the basic identity profile information. A relevant scenario is as follows: the User first logs in to an online service using his/her identity managed by an Identity Provider. Then, the online service asks the Attribute Authority for the additional User’s attributes (e.g., entitlements) before granting access to its resources. In some high-sensitive cases, an Attribute Authority needs proof of the User’s authentication before releasing the User’s attributes to the online service. The challenge of this scenario involving usability, security, and privacy requirements lies in finding the right mechanism to share (the minimum and necessary set of) claims of the User who is currently authenticated with the online service across multiple domains without requiring his or her re-authentication. In this paper, we present the design of two solutions based on OpenID Connect to share User claims across domains. We provide security and privacy analysis for the two solutions and a brief comparison between them. 
  destination: ARES2023
  year: 2023
  doi: 10.1145/3600160.3600183
  urlNews: /news/2023/05/15/paper-accepted-at-ares-2023/
  
- id: COSE2023
  id_iris: 337867
  title: "Identifying and Quantifying Trade-offs in Multi-Stakeholder Risk Evaluation with Applications to the Data Protection Impact Assessment of the GDPR"
  authors:
    - MajidMollaeefar
    - SilvioRanise
  abstract: >
    Cybersecurity risk management consists of several steps including the selection of appropriate controls to minimize risks.  
    This is a difficult task that requires to search through all possible subsets of a set of available controls and identify those that minimize the risks of all stakeholders.
    Since stakeholders may have different perceptions of the risks (especially when considering the impact of threats), conflicting goals may arise that require to find the best possible trade-offs among the various needs.
    In this work, we propose a quantitative and (semi-)automated approach to solve this problem based on the well-known notion of Pareto optimality.  For validation, we show how a prototype tool based on our approach can assist in the Data Protection Impact Assessment mandated by the General Data Protection Regulation on a simplified-but realistic-use case scenario.  We also evaluate the scalability of the approach by conducting an experimental evaluation with the prototype with encouraging results.
  destination: COSE
  year: 2023
  doi: 10.1016/j.cose.2023.103206
  urlNews: /news/2023/03/28/paper-accepted-at-cose/
  
- id: DBSEC2023
  id_iris: 339007
  title: "Assurance, Consent and Access Control for Privacy-Aware OIDC Deployments"
  authors:
    - GianlucaSassetti
    - AmirSharif
    - GiadaSciarretta
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    The large amount of personal data that is shared in the digital age has proportionally increased the risks of user privacy violations. The same privacy risks are reflected in OpenID Connect, which is one of the most widespread protocols used for identity management to access both private and public administration services. Since personal data is collected and shared via OpenID Connect, appropriate technologies to protect user privacy should be adopted as suggested by data protection guidelines and regulations (e.g., the General Data Protection Regulation). Unfortunately, it is difficult to make the privacy-enhancing technology suggestions in such documents actionable and available to IT professionals who are required to configure them within their OpenID Connect deployments. To overcome this problem, we present a practical approach to improving user privacy in OpenID Connect-based solutions by identifying a set of privacy-preserving features extracted from the available OpenID Connect specifications. We conduct a privacy compliance analysis on popular private and governmental OpenID Providers to determine how widely these privacy best practices are used in the wild. The findings indicate that different OpenID Providers grant varying levels of assurance and address different aspects of privacy, failing to provide full support for data protection principles. 
  destination: DBSEC2023
  year: 2023
  doi: 10.1007/978-3-031-37586-6_13
  urlNews: /news/2023/05/25/paper-accepted-at-dbsec-2023/

- id: DBSEC2023_WalletTrends
  id_iris: 339507
  title: "Control is Nothing Without Trust a First Look into Digital Identity Wallet Trends"
  authors:
    - ZahraEbadiAnsaroudi
    - RobertoCarbone
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    In recent years, user-centric digital identity wallets have become increasingly available, aiming to give individuals direct control over their personal data. The EU proposal in the context of the recently revised eIDAS and its EU digital identity wallet reflects the high ambitions in this field at the EU level. However, to the best of our knowledge, no research review on the core technologies used to implement various features of these wallet solutions has been proposed so far. Our work addresses this issue providing a systematic analysis of a selection of available digital identity wallets on the market in terms of the technologies used to establish trust and controlled sharing. Building on this overview and help providers (including companies and European Member States) in charge of developing secure and trustworthy wallet-based infrastructures, we propose a classification of wallet solutions along two main dimensions (namely trust establishment and controlled credential sharing) with the goal of assisting designers to make informed design decisions and guarantee security, privacy, and trustworthiness.
  destination: DBSEC2023
  year: 2023
  doi: 10.1007/978-3-031-37586-6_7

- id: ECML/PKDD2023_W
  id_iris: 323366
  title: Towards a Fine-Grained Threat Model for Video-Based Remote Identity Proofing
  authors:
    - CeciliaPasquini
    - MarcoPernpruner
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    The attack landscape against video-based face verification is rapidly evolving, thus leading to increased opportunities of impersonation and identity theft within remote identity proofing processes. To support reliable security and risk analyses, we provide an extended threat model composed of threats and security controls for the face acquisition phase. Special emphasis is devoted to recent advancements in video synthesis and physical rendering, as well as diversified approaches for liveness detection.
  destination: ECML/PKDD2023_PP
  year: 2023
  urlNews: /news/2023/11/20/paper-accepted-at-ecml-pkdd-post-workshop-proceedings/

- id: EVOTEID2023
  id_iris: 346347
  year: 2023
  title: "Coercion-resistant i-voting with short PIN and OAuth 2.0"
  authors:
    - MatteoBitussi
    - RiccardoLongo
    - FrancescoAntonioMarino
    - UmbertoMorelli
    - AmirSharif
    - ChiaraSpadafora
    - AlessandroTomasi
  abstract: >
    This paper presents an architecture for an OAuth 2.0-based i-voting solution using a mobile native client in a variant of the Araújo-Traoré protocol. We follow a systematic approach by identifying relevant OAuth 2.0 specifications and best practices. Having defined our framework, we identify threats applicable to our proposed methodology and detail how our design mitigates them to provide a safer i-voting process.
  destination: EVOTEID2023
  #doi: 10.
  tags:                     
    - ThresholdCryptography
    - ZKP
    - SMPC
    - PrivacyEnhancingCryptography
    - DecentralizationOfTrust
    
- id: POLSIM2023
  #id_iris: 323366
  title: "A Simulation Framework for the Experimental Evaluation of Access Control Enforcement Mechanisms based on Business Processes"
  authors:
    - StefanoBerlato
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    While the security analysis of Access Control (AC) policies has received a lot of attention, the same cannot be said for their enforcement. As systems become more distributed (e.g., centralized services may become a bottleneck) and legal compliance constraints stricter (e.g., the problem of honest but curious Cloud providers in the light of privacy regulations), the fine-tuning of AC enforcement mechanisms is likely to become more and more important. This is especially true in scenarios where the quality of service may suffer from computationally heavy security mechanisms and low latency is a prominent requirement. As a first step towards a principled approach to fine-tune AC enforcement, this paper introduces a methodology providing the means to measure the performance of AC enforcement mechanisms through the simulation of realistic deployment scenarios. To do so, we base our methodology on Business Process Model and Notation (BPMN) workflows—that provide for an appropriate abstraction of the sequence of requests toward AC enforcement mechanisms performed by applications—to derive lists of AC operations (e.g., access a resource, revoke a permission) and execute them to evaluate and compare the performance of different mechanisms. Finally, we implement our methodology and apply it to three case studies representative of both traditional centralized AC—i.e., the Open Policy Agent (OPA) and the eXtensible Access Control Markup Language (XACML)—and decentralized Cryptographic Access Control (CAC)—i.e., CryptoAC—.
  destination: POLSIM2023
  year: 2023
  #doi: 10.1145/3320269.3384767
  urlComplementary: /complementary/POLSIM2023
  #urlNews: /news/2020/02/15/paper-accepted-at-asiaccs-2020/

- id: RACS2023
  id_iris: 344627
  title: "SecCo: Automated Services to Secure Containers in the DevOps Paradigm"
  authors:
    - LucaVerderame
    - LucaCaviglione
    - RobertoCarbone
    - AlessioMerlo
  abstract: >
    Containers are core building blocks for creating applications based on the microservice paradigm. However, assessing their security is complex, especially when deployed in distributed and heterogeneous scenarios. Moreover, developers and IT operators should only focus on integration and delivery processes without dealing with tasks to guarantee securing requirements. To overcome such issues, in this paper, we introduce the ideas at the basis of Project SecCo (Securing Containers), i.e., an architecture for extending and improving current security assessment methodologies into the continuous integration and continuous delivery DevOps pipeline. To this end, SecCo proposes a framework able to orchestrate new automatic security services to prevent and reduce security vulnerabilities in the design, implementation, and deployment phases, and to identify and mitigate, at runtime, attempts to exploit them. The paper also showcases the main research challenges to be addressed for pursuing the vision of SecCo.
  destination: RACS2023
  year: 2023
  doi: 10.1145/3599957.3606222

- id: SECRYPT2023
  id_iris: 338307
  title: "A First Appraisal of Cryptographic Mechanisms for the Selective Disclosure of Verifiable Credentials"
  authors:
    - AndreaFlamini
    - SilvioRanise
    - GiadaSciarretta
    - MarioScuro
    - AmirSharif
    - AlessandroTomasi 
  abstract: >
    Verifiable credentials are a digital analogue of physical credentials. Their authenticity and integrity are protected by means of cryptographic techniques, and they can be presented to verifiers to prove claims about the holder of the credential itself. One way to preserve privacy during presentation consists in selectively disclosing the attributes in a credential. In this paper we present the most widespread cryptographic mechanisms used to enable selective disclosure of attributes, describing their structure and comparing them in terms of performance, size of the associated verifiable presentations, and the ability to produce predicate proofs and unlinkable presentations.
  destination: SECRYPT2023
  year: 2023
  doi: 10.5220/0012084000003555
  urlNews: /news/2023/04/24/paper-accepted-at-secrypt-2023/

- id: TDSC2022
  id_iris: 342587
  title: "An Automated Multi-Layered Methodology to Assist the Secure and Risk-Aware Design of Multi-Factor Authentication Protocols"
  authors:
    - MarcoPernpruner
    - RobertoCarbone
    - GiadaSciarretta
    - SilvioRanise
  abstract: >
    Authentication protocols represent the entry point to online services, so they must be sturdily designed in order to allow only authorized users to access the underlying data. However, designing authentication protocols is a complex process: security designers should carefully select the technologies to involve and integrate them properly in order to prevent potential vulnerabilities. In addition, these choices are usually restricted by further factors, such as the requirements associated with the scenario, the regulatory framework, the dimensions to balance (e.g., security vs. usability), and the standards to rely on. We come to the rescue by presenting an automated multi-layered methodology we have developed to assist security designers in this phase: by repeatedly evaluating their protocols, they can select the security mitigations to consider until they reach the desired security level, thus enabling a security-by-design approach. For concreteness, we also show how we have applied our methodology to a real use case scenario in the context of a collaboration with the Italian Government Printing Office and Mint.
  destination: TDSC
  destinationAddon: Volume 21, Issue 4, July/August 2024, Pages 1935-1950
  year: 2024
  doi: 10.1109/TDSC.2023.3296210
  urlComplementary: /complementary/TDSC2022
  urlNews: /news/2023/07/17/paper-accepted-at-tdsc/

## 2024
- id: EUROSP2024
  title: "CSRF-ing the SSO waves: security testing of SSO-based account linking process"
  authors:
    - AndreaBisegna
    - MatteoBitussi
    - RobertoCarbone
    - LucaCompagna
    - SilvioRanise
    - AvinashSudhodanan
  abstract:
  destination: EUROSP2024
  year: 2024

- id: Ital-IA2024
  title: "A Risk-based Approach to Trustworthy AI Systems for Judicial Procedures"
  authors:
    - MajidMollaeefar
    - EleonoraMarchesini
    - RobertoCarbone
    - SilvioRanise
  abstract: >
    In the rapidly evolving landscape of Artificial Intelligence (AI), ensuring the trustworthiness of AI tools deployed in sensitive use cases, such as judicial or healthcare processes, is paramount. The management of AI risks in judicial systems necessitates a holistic approach that includes various elements, such as technical, ethical considerations, and legal responsibilities. This approach should not only involve the application of risk management frameworks and regulations but also focus on the education and training of legal professionals. For this, we propose a risk-based approach designed to evaluate and mitigate potential risks associated with AI applications in judicial settings. Our approach is a semi-automated process that integrates both user (i.e., judge) feedback and technical insights to assess the AI tool’s alignment with Trustworthy AI principles.
  destination: Ital-IA2024
  year: 2024
  urlNews: /news/2024/04/24/paper-accepted-at-ital-ia-2024/
 
- id: JISA2024
  id_iris: 347387
  title: On Cryptographic Mechanisms for the Selective Disclosure of Verifiable Credentials
  authors:
    - AndreaFlamini
    - GiadaSciarretta
    - MarioScuro
    - AmirSharif
    - AlessandroTomasi
    - SilvioRanise
  abstract: >
    Verifiable credentials are a digital analogue of physical credentials. Their authenticity and integrity are protected by means of cryptographic techniques, and they can be presented to verifiers to reveal attributes or even predicates about the attributes included in the credential.
    One way to preserve privacy during presentation consists in selectively disclosing the attributes in a credential. In this paper we present the most widespread cryptographic mechanisms used to enable selective disclosure of attributes identifying two categories: the ones based on hiding commitments - e.g., mdl ISO/IEC 18013-5 - and the ones based on non-interactive zero-knowledge proofs - e.g., BBS signatures. We also include a description of the cryptographic primitives used to design such cryptographic mechanisms.
    We describe the design of the cryptographic mechanisms and compare them by performing an analysis on their standard maturity in terms of standardization, cryptographic agility and quantum safety, then we compare the features that they support with main focus on the unlinkability of presentations, the ability to create predicate proofs and support for threshold credential issuance.
    Finally we perform an experimental evaluation based on the Rust open source implementations that we have considered most relevant. In particular we evaluate the size of credentials and presentations built using different cryptographic mechanisms and the time needed to generate and verify them. We also highlight some trade-offs that must be considered in the instantiation of the cryptographic mechanisms.
  destination: JISA
  year: 2024
  doi: 10.1016/j.jisa.2024.103789
  urlNews: /news/2024/05/10/paper-accepted-at-jisa/

- id: SECRYPT2024
  id_iris: 348308
  title: "Automating Compliance for Improving TLS Security Postures: An Assessment of Public Administration Endpoints"
  authors:
    - RiccardoGermenia
    - SalvatoreManfredi
    - MatteoRizzi
    - GiadaSciarretta
    - AlessandroTomasi
    - SilvioRanise
  abstract: >
    System administrators tasked with configuring TLS servers must make numerous decisions - e.g., selecting the appropriate ciphers, signature algorithms, and TLS extensions - and it may not be obvious, even to security experts, which decisions may expose to attacks. To address this issue, raise awareness, and establish a security threshold, numerous cybersecurity agencies around the world issue technical guidelines for the use and configuration of TLS. 
    In this paper we carry out an assessment of the TLS security posture of European and US based endpoints in relation to their respective national cybersecurity guidelines. Our results show that compliance levels are insufficient, as only a fraction of these recommendations are successfully implemented. We attempt to identify potential causes by presenting a series of observations that may underlie the lack of compliance.
    The analysis is conducted by employing a TLS analyzer we developed to automate the compliance analysis and the application of the suggested changes, assisting system administrators during this important yet complex task.
    Our tool and the dataset containing the machine-readable requirements for automating conformity assessment are publicly available, thus making the process auditable and the assets extensible.
  destination: SECRYPT2024
  year: 2024
  doi: 10.5220/0012764700003767
  urlComplementary: /complementary/SECRYPT2024
  urlNews: /news/2024/04/22/paper-accepted-at-secrypt-2024/

- id: TOSEM2024
  id_iris: 344227
  title: "Mitigating Debugger-based Attacks to Java Applications with Self-Debugging"
  authors:
    - StefanoBerlato
    - DavidePizzolotto
    - MarianoCeccato
  abstract: >
    Java bytecode is a quite high-level language and, as such, it is fairly easy to analyze and decompile with malicious intents, e.g., to tamper with code and skip license checks. Code obfuscation was a first attempt to mitigate malicious reverse engineering based on static analysis. However, obfuscated code can still be dynamically analyzed with standard debuggers to perform step-wise execution and to inspect (or change) memory content at important execution points, e.g., to alter the verdict of license validity checks. Although some approaches have been proposed to mitigate debugger-based attacks, they are only applicable to binary compiled code and none address the challenge of protecting Java bytecode. In this paper, we propose a novel approach to protect Java bytecode from malicious debugging. Our approach is based on automated program transformation to manipulate Java bytecode and split it into two binary processes that debug each other (i.e., a self-debugging solution). In fact, when the debugging interface is already engaged, an additional malicious debugger cannot attach. To be resilient against typical attacks, our approach adopts a series of technical solutions, e.g., an encoded channel is shared by the two processes to avoid leaking information, an authentication protocol is established to avoid Man-in-the-Middle attacks and the computation is spread between the two processes to prevent the attacker to replace or terminate either of them. We test our solution on 18 real-world Java applications, showing that our approach can effectively block the most common debugging tasks (either with the Java debugger or the GNU debugger) while preserving the functional correctness of the protected programs. While the final decision on when to activate this protection is still up to the developers, the observed performance overhead was acceptable for common desktop application domains.
  destination: TOSEM
  year: 2024
  doi: 10.1145/3631971

# PLEASE KEEP ALPHABETICAL ORDER BY ID WITHIN YEARS