1,721,222 research outputs found
On the verification of security-aware E-services
No full textAbstractWeb 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
Symbolic Backward Reachability with Effectively Propositional Logic-Applications to Security Policy Analysis
No full textSatisfiability solving for software verification
No full textDeclarative techniques for software verification require the availability of scalable, predictable, and flexible satisfiability solvers. We describe our approach to build such solvers by combining equational theorem proving, Boolean solving, arithmetic reasoning, and some transformations of the proof obligations. The proposed techniques have been implemented in a system called haRVey and the viability of the approach is shown on proof obligations generated in the certification of aerospace code
Verification of Composed Array-based Systems with Applications to Security-Aware Workflows
No full textFrontiers of Combining Systems, 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings
No full textThis book constitutes the proceedings of the 10th International Symposium on Frontiers of Combining Systems, FroCoS 2015, held in Wroclaw, Poland, in September 2015.
The 20 papers presented in this volume were carefully reviewed and selected from 34 submissions. They were organized in topical sections named: description logics; theorem proving and model building; decision procedures; decision procedures for verification; rewriting and constraint solving; transformations between symbolic systems; combination methods; and reasoning in large theories. The book also contains one invited talk in full-paper length
A Tool-assisted Methodology for the Data Protection Impact Assessment
No full textWe 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
Building Extended Canonizers by Graph-Based Deduction
No full textWe consider the problem of efficiently building extended canonizers, which are capable of solving the uniform word problem for some first-order theories. These reasoning artifacts have been introduced in previous work to solve the lack of modularity of Shostak combination schema while retaining its efficiency. It is known that extended canonizers can be modularly combined to solve the uniform word problem in unions of theories. Unfortunately, little is known about efficiently implementing such canonizers for component theories, especially those of interest for verification like, e.g., those of uninterpreted function symbols or lists. In this paper, we investigate this problem by adapting and combining work on rewriting-based decision procedures for satisfiability in first-order theories and SER graphs, a graph-based method defined for abstract congruence closure. Our goal is to build graph-based extended canonizers for theories which are relevant for verification. Based on graphs our approach addresses implementation issues that were lacking in previous rewriting-based decision procedure approaches and which are important to argue the viability of extended canonizers
A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic
No full textIn this paper, we propose a generic mechanism for extending decision procedures by means of a lemma speculation mechanism. This problem is important in order to widen the scope of decision procedures incorporated in state-of-the-art verification systems. Soundness and termination of the extension schema are formally stated and proved. As a case study, we consider extensions of a decision procedure for the quantifier-free fragment of Presburger Arithmetic to significant fragments of non-linear arithmetic
Assessing the Effectiveness of the Shared Responsibility Model for Cloud Databases: the Case of Google’s Firebase
Full text linkMigrating 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
- …
