References of "Bianculli, Domenico 50000779"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailSecurity Slicing for Auditing Common Injection Vulnerabilities
Thome, Julian UL; Shar, Lwin Khin UL; Bianculli, Domenico UL et al

in The Journal of Systems & Software (in press)

Cross-site scripting and injection vulnerabilities are among the most common and serious security issues for Web applications. Although existing static analysis approaches can detect potential ... [more ▼]

Cross-site scripting and injection vulnerabilities are among the most common and serious security issues for Web applications. Although existing static analysis approaches can detect potential vulnerabilities in source code, they generate many false warnings and source-sink traces with irrelevant information, making their adoption impractical for security auditing. One suitable approach to support security auditing is to compute a program slice for each sink, which contains all the information required for security auditing. However, such slices are likely to contain a large amount of information that is irrelevant to security, thus raising scalability issues for security audits. In this paper, we propose an approach to assist security auditors by defining and experimenting with pruning techniques to reduce original program slices to what we refer to as security slices, which contain sound and precise information. To evaluate the proposed approach, we compared our security slices to the slices generated by a state-of-the-art program slicing tool, based on a number of open-source benchmarks. On average, our security slices are 76% smaller than the original slices. More importantly, with security slicing, one needs to audit approximately 1% of the total code to fix all the vulnerabilities, thus suggesting significant reduction in auditing costs. [less ▲]

Detailed reference viewed: 204 (32 UL)
Full Text
Peer Reviewed
See detailOn the Risk of Tool Over-tuning in Runtime Verification Competitions
Bianculli, Domenico UL; Krstic, Srdan

in Proceedings of RV-CUBES 2017: an International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (in press)

Detailed reference viewed: 11 (0 UL)
Full Text
Peer Reviewed
See detailTemPsy-Check: a Tool for Model-driven Trace Checking of Pattern-based Temporal Properties
Dou, Wei; Bianculli, Domenico UL; Briand, Lionel UL

in Proceedings of RV-CUBES 2017: an International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (in press)

Detailed reference viewed: 12 (0 UL)
Full Text
Peer Reviewed
See detailThe Case for Context-Driven Software Engineering Research
Briand, Lionel UL; Bianculli, Domenico UL; Nejati, Shiva UL et al

in IEEE Software (in press)

Detailed reference viewed: 91 (10 UL)
Full Text
Peer Reviewed
See detailJoanAudit: A Tool for Auditing Common Injection Vulnerabilities
Thome, Julian UL; Shar, Lwin Khin UL; Bianculli, Domenico UL et al

in 11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (2017, September)

JoanAudit is a static analysis tool to assist security auditors in auditing Web applications and Web services for common injection vulnerabilities during software development. It automatically identifies ... [more ▼]

JoanAudit is a static analysis tool to assist security auditors in auditing Web applications and Web services for common injection vulnerabilities during software development. It automatically identifies parts of the program code that are relevant for security and generates an HTML report to guide security auditors audit the source code in a scalable way. JoanAudit is configured with various security-sensitive input sources and sinks relevant to injection vulnerabilities and standard sanitization procedures that prevent these vulnerabilities. It can also automatically fix some cases of vulnerabilities in source code — cases where inputs are directly used in sinks without any form of sanitization — by using standard sanitization procedures. Our evaluation shows that by using JoanAudit, security auditors are required to inspect only 1% of the total code for auditing common injection vulnerabilities. The screen-cast demo is available at https://github.com/julianthome/joanaudit. [less ▲]

Detailed reference viewed: 86 (25 UL)
Full Text
Peer Reviewed
See detailA Model-Driven Approach to Trace Checking of Pattern-based Temporal Properties
Dou, Wei; Bianculli, Domenico UL; Briand, Lionel UL

in Proceedings of the ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS 2017 ) (2017, September)

Detailed reference viewed: 34 (4 UL)
Full Text
See detailAn Integrated Approach for Effective Injection Vulnerability Analysis of Web Applications through Security Slicing and Hybrid Constraint Solving
Thome, Julian UL; Shar, Lwin Khin UL; Bianculli, Domenico UL et al

Report (2017)

Malicious users can attack Web applications by exploiting injection vulnerabilities in the source code. This work addresses the challenge of detecting injection vulnerabilities in a scalable and effective ... [more ▼]

Malicious users can attack Web applications by exploiting injection vulnerabilities in the source code. This work addresses the challenge of detecting injection vulnerabilities in a scalable and effective way. We propose an integrated approach that seamlessly combines security slicing with hybrid constraint solving, i.e., constraint solving based on a combination of automata-based solving and meta-heuristic search. We use static analysis to extract minimal program slices relevant to security from Web programs and to generate attack conditions. We then apply hybrid constraint solving to determine the satisfiability of attack conditions and thus detect vulnerabilities. The experimental results, using a benchmark suite comprising nine diverse and representative Web applications, show that our approach (implemented in the JOACO tool) is significantly more effective at detecting injection vulnerabilities than state-of-the-art approaches, achieving 98% recall, without producing any false alarm. We also compared the constraint solving module of our approach with state-of-the-art constraint solvers, using five different benchmark suites; our approach correctly solved the highest number of constraints (43177 out of 43184), without producing any incorrect result, and was the one with the least number of time-out/failing cases. In both scenarios, the execution time was practically acceptable, given the offline nature of vulnerability detection. [less ▲]

Detailed reference viewed: 25 (0 UL)
Full Text
Peer Reviewed
See detailSearch-driven String Constraint Solving for Vulnerability Detection
Thome, Julian UL; Shar, Lwin Khin UL; Bianculli, Domenico UL et al

in Proceedings of the 39th International Conference on Software Engineering (ICSE 2017) (2017, May)

Constraint solving is an essential technique for detecting vulnerabilities in programs, since it can reason about input sanitization and validation operations performed on user inputs. However, real-world ... [more ▼]

Constraint solving is an essential technique for detecting vulnerabilities in programs, since it can reason about input sanitization and validation operations performed on user inputs. However, real-world programs typically contain complex string operations that challenge vulnerability detection. State-of-the-art string constraint solvers support only a limited set of string operations and fail when they encounter an unsupported one; this leads to limited effectiveness in finding vulnerabilities. In this paper we propose a search-driven constraint solving technique that complements the support for complex string operations provided by any existing string constraint solver. Our technique uses a hybrid constraint solving procedure based on the Ant Colony Optimization meta-heuristic. The idea is to execute it as a fallback mechanism, only when a solver encounters a constraint containing an operation that it does not support. We have implemented the proposed search-driven constraint solving technique in the ACO-Solver tool, which we have evaluated in the context of injection and XSS vulnerability detection for Java Web applications. We have assessed the benefits and costs of combining the proposed technique with two state-of-the-art constraint solvers (Z3-str2 and CVC4). The experimental results, based on a benchmark with 104 constraints derived from nine realistic Web applications, show that our approach, when combined in a state-of-the-art solver, significantly improves the number of detected vulnerabilities (from 4.7% to 71.9% for Z3-str2, from 85.9% to 100.0% for CVC4), and solves several cases on which the solver fails when used stand-alone (46 more solved cases for Z3-str2, and 11 more for CVC4), while still keeping the execution time affordable in practice. [less ▲]

Detailed reference viewed: 627 (61 UL)
Full Text
Peer Reviewed
See detailGemRBAC-DSL: a High-level Specification Language for Role-based Access Control Policies
Ben Fadhel, Ameni UL; Bianculli, Domenico UL; Briand, Lionel UL

in 21st ACM Symposium on Access Control Models and Technologies (SACMAT 2016) (2016, June)

A role-based access control (RBAC) policy restricts a user to perform operations based on her role within an organization. Several RBAC models have been proposed to represent different types of RBAC ... [more ▼]

A role-based access control (RBAC) policy restricts a user to perform operations based on her role within an organization. Several RBAC models have been proposed to represent different types of RBAC policies. However, the expressiveness of these models has not been matched by specification languages for RBAC policies. Indeed, existing policy specification languages do not support all the types of RBAC policies defined in the literature. In this paper we aim to bridge the gap between highly-expressive RBAC models and policy specification languages, by presenting GemRBAC-DSL, a new specification language designed on top of an existing, generalized conceptual model for RBAC. The language sports a syntax close to natural language, to encourage its adoption among practitioners. We also define semantic checks to detect conflicts and inconsistencies among the policies written in a GemRBAC-DSL specification. We show how the semantics of GemRBAC-DSL can be expressed in terms of an existing formalization of RBAC policies as OCL (Object Constraint Language) constraints on the corresponding RBAC conceptual model. This formalization paves the way to define a model-driven approach for the enforcement of policies written in GemRBAC-DSL. [less ▲]

Detailed reference viewed: 139 (21 UL)
Full Text
Peer Reviewed
See detailEfficient Large-scale Trace Checking Using MapReduce
Bersani, Marcello Maria; Bianculli, Domenico UL; Ghezzi, Carlo et al

in Proceedings of the 38th International Conference on Software Engineering (ICSE 2016) (2016, May)

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic ... [more ▼]

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval for which logged events must be buffered to check satisfaction of the specification. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches. In this paper we address this memory scalability issue by proposing a new semantics for MTL, called lazy semantics. This semantics can evaluate temporal formulae and boolean combinations of temporal-only formulae at any arbitrary time instant. We prove that lazy semantics is more expressive than standard point-based semantics and that it can be used as a basis for a correct parametric decomposition of any MTL formula into an equivalent one with smaller, bounded time intervals. We use lazy semantics to extend our previous distributed trace checking algorithm for MTL. We evaluate the proposed algorithm in terms of memory scalability and time/memory tradeoffs. [less ▲]

Detailed reference viewed: 128 (12 UL)
Full Text
Peer Reviewed
See detailTesting the Untestable: Model Testing of Complex Software-Intensive Systems
Briand, Lionel UL; Nejati, Shiva UL; Sabetzadeh, Mehrdad UL et al

in Proceedings of the 38th International Conference on Software Engineering (ICSE 2016) Companion (2016, May)

Detailed reference viewed: 356 (39 UL)
Full Text
See detailGemRBAC-DSL: a High-level Specification Language for Role-based Access Control Policies
Ben Fadhel, Ameni UL; Bianculli, Domenico UL; Briand, Lionel UL

Report (2016)

A role-based access control (RBAC) policy restricts a user to perform operations based on her role within an organization. Several RBAC models have been proposed to represent different types of RBAC ... [more ▼]

A role-based access control (RBAC) policy restricts a user to perform operations based on her role within an organization. Several RBAC models have been proposed to represent different types of RBAC policies. However, the expressiveness of these models has not been matched by specification languages for RBAC policies. Indeed, existing policy specification languages do not support all the types of RBAC policies defined in the literature. In this paper we aim to bridge the gap between highly-expressive RBAC models and policy specification languages, by presenting GemRBAC-DSL, a new specification language designed on top of an existing, generalized conceptual model for RBAC. The language sports a syntax close to natural language, to encourage its adoption among practitioners. We also define semantic checks to detect conflicts and inconsistencies among the policies written in a GemRBAC-DSL specification. We show how the semantics of GemRBAC-DSL can be expressed in terms of an existing formalization of RBAC policies as OCL (Object Constraint Language) constraints on the corresponding RBAC conceptual model. This formalization paves the way to define a model-driven approach for the enforcement of policies written in GemRBAC-DSL. [less ▲]

Detailed reference viewed: 95 (17 UL)
Full Text
Peer Reviewed
See detailA model-driven approach to representing and checking RBAC contextual policies.
Ben Fadhel, Ameni UL; Bianculli, Domenico UL; Briand, Lionel UL et al

in Proceedings of the 6th ACM Conference on Data and Application Security and Privacy (CODASPY 2016) (2016, March)

Detailed reference viewed: 189 (22 UL)
Full Text
Peer Reviewed
See detailA Comprehensive Modeling Framework for Role-based Access Control Policies
Ben Fadhel, Ameni UL; Bianculli, Domenico UL; Briand, Lionel UL

in The Journal of Systems & Software (2015), 107(September,2015), 110126

Prohibiting unauthorized access to critical resources and data has become a major requirement for enter- prises; access control (AC) mechanisms manage requests from users to access system resources. One ... [more ▼]

Prohibiting unauthorized access to critical resources and data has become a major requirement for enter- prises; access control (AC) mechanisms manage requests from users to access system resources. One of the most used AC paradigms is role-based access control (RBAC), in which access rights are determined based on the user’s role. Many different types of RBAC policies have been proposed in the literature, each one accompanied by the corresponding extension of the original RBAC model. However, there is no unified framework that can be used to define all these types of policies in a coherent way, using a common model. In this paper we propose a model-driven engineering approach, based on UML and the Object Constraint Language (OCL), to enable the precise specification and verification of such policies. More specifically, we first present a taxonomy of the various types of RBAC policies proposed in the literature. We also propose the GemRBAC model, a generalized model for RBAC that includes all the entities required to define the classified policies. This model is a conceptual model that can also serve as data model to operationalize data collection and verification. Lastly, we formalize the classified policies as OCL constraints on the GemRBAC model. [less ▲]

Detailed reference viewed: 191 (36 UL)
Full Text
Peer Reviewed
See detailSyntax-driven program verification of matching logic properties.
Bianculli, Domenico UL; Filieri, Antonio; Ghezzi, Carlo et al

in Proceedings of the 3rd FME Workshop on Formal Methods in Software Engineering (FormaliSE 2015) (2015, May)

Detailed reference viewed: 43 (4 UL)
Full Text
Peer Reviewed
See detailSyntactic-Semantic Incrementality for Agile Verification
Bianculli, Domenico UL; Filieri, Antonio; Ghezzi, Carlo et al

in Science of Computer Programming (2015), 97(0), 47-54

Modern software systems are continuously evolving, often because systems requirements change over time. Responding to requirements changes is one of the principles of agile methodologies. In this paper we ... [more ▼]

Modern software systems are continuously evolving, often because systems requirements change over time. Responding to requirements changes is one of the principles of agile methodologies. In this paper we envision the seamless integration of automated verification techniques within agile methodologies, thanks to the support for incrementality. Incremental verification accommodates the changes that occur within the schedule of frequent releases of software agile processes. We propose a general approach to developing families of verifiers that can support incremental verification for different kinds of artifacts and properties. The proposed syntactic-semantic approach is rooted in operator precedence grammars and their support for incremental parsing. Incremental verification procedures are encoded as attribute grammars, whose incremental evaluation goes hand in hand with incremental parsing. [less ▲]

Detailed reference viewed: 134 (27 UL)
Full Text
Peer Reviewed
See detailOffline Trace Checking of Quantitative Properties of Service-Based Applications
Bianculli, Domenico UL; Ghezzi, Carlo; Krstić, Srđan et al

in Proceedings of the 7h International Conference on Service Oriented Computing and Application (SOCA 2014) (2014, November)

Detailed reference viewed: 23 (2 UL)
Full Text
See detailA Comprehensive Modeling Framework for Role-based Access Control Policies
Ben Fadhel, Ameni UL; Bianculli, Domenico UL; Briand, Lionel UL

Report (2014)

Prohibiting unauthorized access to critical resources and data has become a major requirement for enterprises. Access control (AC) mechanisms manage requests from users to access system resources; the ... [more ▼]

Prohibiting unauthorized access to critical resources and data has become a major requirement for enterprises. Access control (AC) mechanisms manage requests from users to access system resources; the access is granted or denied based on authorization policies defined within the enterprise. One of the most used AC paradigms is role-based access control (RBAC). In RBAC, access rights are determined based on the user's role, e.g., her job or function in the enterprise. Many different types of RBAC authorization policies have been proposed in the literature, each one accompanied by the corresponding extension of the original RBAC model. However, there is no unified framework that can be used to define all these types of RBAC policies in a coherent way, using a common model. Moreover, these types of policies and their corresponding models are scattered across multiple sources and sometimes the concepts are expressed ambiguously. This situation makes it difficult for researchers to understand the state of the art in a coherent manner; furthermore, practitioners may experience severe difficulties when selecting the relevant types of policies to be implemented in their systems based on the available information. There is clearly a need for organizing the various types of RBAC policies systematically, based on a unified framework, and to formalize them to enable their operationalization. In this paper we propose a model-driven engineering (MDE) approach, based on UML and the Object Constraint Language (OCL), to enable the precise specification and verification of such policies. More specifically, we first present a taxonomy of the various types of RBAC authorization policies proposed in the literature. We also propose the GemRBAC model, a generalized model for RBAC that includes all the entities required to define the classified policies. This model is a conceptual model that can also serve as data model to operationalize data collection and verification. Lastly, we formalize the classified RBAC policies as OCL constraints on the GemRBAC model. To facilitate such operationalization, we make publicly available online the ECore version of the GemRBAC model and the OCL constraints corresponding to the classified RBAC policies. [less ▲]

Detailed reference viewed: 417 (169 UL)
Full Text
Peer Reviewed
See detailIncremental Syntactic-Semantic Reliability Analysis of Evolving Structured Workflows
Bianculli, Domenico UL; Filieri, Antonio; Ghezzi, Carlo et al

in Proceedings of the 6th International Symposium On Leveraging Applications of Formal Methods Verification and Validation (ISoLA 2014) (2014, October)

Detailed reference viewed: 13 (0 UL)