References of "Bianculli, Domenico 50000779"
     in
Bookmark and Share    
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 (2017), 34(5), 72-75

Detailed reference viewed: 383 (32 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: 195 (20 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: 936 (81 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: 268 (26 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: 318 (24 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: 654 (52 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: 207 (24 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: 329 (32 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 Journal of Systems and Software (2015), 107(September,2015), 110-126

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: 464 (60 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: 151 (7 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: 243 (34 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: 764 (178 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: 124 (3 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: 98 (1 UL)
Full Text
Peer Reviewed
See detailTrace checking of Metric Temporal Logic with Aggregating Modalities using MapReduce
Bianculli, Domenico UL; Ghezzi, Carlo; Krstić, Srđan

in Proceedings of the 12th International Conference on Software Engineering and Formal Methods (SEFM 2014) (2014, September)

Detailed reference viewed: 159 (13 UL)
Full Text
Peer Reviewed
See detailRevisiting Model-driven Engineering for Run-time Verification of Business Processes
Dou, Wei UL; Bianculli, Domenico UL; Briand, Lionel UL

in Proceedings of the 8th System Analysis and Modeling Conference (SAM 2014) (2014, September)

Detailed reference viewed: 208 (25 UL)
Full Text
Peer Reviewed
See detailOCLR: a More Expressive, Pattern-based Temporal Extension of OCL
Dou, Wei UL; Bianculli, Domenico UL; Briand, Lionel UL

in Proceedings of the 2014 European Conference on Modelling Foundations and Applications (ECMFA 2014) (2014, July)

Detailed reference viewed: 230 (22 UL)
Full Text
See detailA Model-Driven Approach to Offline Trace Checking of Temporal Properties with OCL
Dou, Wei UL; Bianculli, Domenico UL; Briand, Lionel UL

Report (2014)

Offline trace checking is a procedure for evaluating requirements over a log of events produced by a system. The goal of this paper is to present a practical and scalable solution for the offline checking ... [more ▼]

Offline trace checking is a procedure for evaluating requirements over a log of events produced by a system. The goal of this paper is to present a practical and scalable solution for the offline checking of the temporal requirements of a system, which can be used in contexts where model-driven engineering is already a practice, where temporal specifications should be written in a domain-specific language not requiring a strong mathematical background, and where relying on standards and industry-strength tools for property checking is a fundamental prerequisite. The main contributions are: the TemPsy language, a domain-specific specification language based on common property specification patterns, and extended with new constructs; a model-driven offline trace checking procedure based on the mapping of requirements written in TemPsy into OCL (Object Constraint Language) constraints on a conceptual model on execution traces, which can be evaluated using an OCL checker; the implementation of this trace checking procedure in the TemPsy-Check tool; the evaluation of the scalability of TemPsy-Check and its comparison to a state-of-the-art alternative technology. The proposed approach has been applied to a case study developed in collaboration with a public service organization, active in the domain of business process modeling for eGovernment. [less ▲]

Detailed reference viewed: 502 (129 UL)
Full Text
See detailOCLR: a More Expressive, Pattern-based Temporal Extension of OCL
Dou, Wei UL; Bianculli, Domenico UL; Briand, Lionel UL

Report (2014)

Modern enterprise information systems often require to specify their functional and non-functional (e.g., Quality of Service) requirements using expressions that contain temporal constraints ... [more ▼]

Modern enterprise information systems often require to specify their functional and non-functional (e.g., Quality of Service) requirements using expressions that contain temporal constraints. Specification approaches based on temporal logics demand a certain knowledge of mathematical logic, which is difficult to find among practitioners; moreover, tool support for temporal logics is limited. On the other hand, a standard language such as the Object Constraint Language (OCL), which benefits from the availability of several industrial-strength tools, does not support temporal expressions. In this paper we propose OCLR, an extension of OCL with support for temporal constraints based on well-known property specification patterns. With respect to previous extensions, we add support for referring to a specific occurrence of an event as well as for indicating a time distance between events and/or scope boundaries. The proposed extension defines a new syntax, very close to natural language, paving the way for a rapid adoption by practitioners. We show the application of the language in a case study in the domain of eGovernment, developed in collaboration with a public service partner. [less ▲]

Detailed reference viewed: 363 (87 UL)