12 KiB
12 KiB
tags:: #zotero title:: @STAF_2025_paper_42 item-type:: journalArticle original-title:: STAF_2025_paper_42 language:: en authors:: Issam Al-Azzoni, Reiko Heckel, Zobia Erum library-catalog:: Zotero links:: Local library, Web library
- Abstract
- Domain-specific languages (DSLs) express requirements or designs, often through visual abstractions. To be effective and reliable for complex development tasks such as code generation, testing and analysis, DSLs need semantic foundations. This paper introduces a model-based framework for testing and analysis based on operational semantics for DSLs expressed through graph rewriting.
-
Attachments
- PDF {{zotero-imported-file RLWLKNXC, "Al-Azzoni et al. - Graph rewriting for testing domain-specific models dynamic role-based access control.pdf"}}
-
Notes
-
Annotazioni
(24/3/2025, 11:45:46)
- “DSLs need semantic foundations.” (Al-Azzoni et al., p. 1) #5fb236
-
- “model-based framework for testing and analysis” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “operational semantics for DSLs expressed through graph rewriting” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “role-based access control models (RBACMs)” (Al-Azzoni et al., p. 1) #e56eee
* *
- “constraints on who can access which resources under a dynamic notion of role membership.” (Al-Azzoni et al., p. 1) #5fb236
* *
- “access control policies for smart contracts involve multiple parties that are members of different groups or organisations” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “DSL for multi-party role-based access control policies which is defined as an extension of the iContractML 2.0 metamodel.” (Al-Azzoni et al., p. 1) #a28ae5
*What is iContractML? *
- “The diagrammatic notation supports complex authorisation patterns, including alternatives and multiplicities, to address the nuanced access control requirements of smart contract applications.” (Al-Azzoni et al., p. 1) #5fb236
* *
- “Groove model checker” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “Digital Asset Modelling Language (DAML).” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “We use an extended model to validate dynamic access control scenarios generated by ChatGPT.” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “Smart contracts support workflows of multiple parties without the need for a central authority” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “smart contracts implement platformspecific access control mechanisms,” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “role-based access control (” (Al-Azzoni et al., p. 1) #5fb236
* *
- “multiparty authorisation,” (Al-Azzoni et al., p. 1) #5fb236
* *
- “hard to understand and verify against security requirements at code level, leaving applications open to data leaks and unauthorised access” (Al-Azzoni et al., p. 1) #a28ae5
* *
- “approach to testing and validating access control policies (ACPs).” (Al-Azzoni et al., p. 1) #e56eee
* *
- “The metamodel and the diagrammatic language it defines help developers to understand and review multi-party RBAC models.” (Al-Azzoni et al., p. 2) #5fb236
* *
- “dynamic RBAC, where dedicated role owners are authorised to add and remove members at runtime.” (Al-Azzoni et al., p. 2) #5fb236
*SO the dynamism is related to the possibility of adding or removing members at runtime ? *
- “homework grading authorised by an individually assigned grader together with either a second named grader or two members of a role of evaluators.” (Al-Azzoni et al., p. 2) #5fb236
* *
- “modelling concepts for roles, role membership, alternatives and cardinalities for authorisation relations and map such models to the smart contract language DAML1 which supports multi-party authorisation but no roles nor alternatives.” (Al-Azzoni et al., p. 2) #2ea8e5
* *
- “Solidity use assertions for access control but do not support multi-party authorisations.” (Al-Azzoni et al., p. 2) #5fb236
* *
- “access control but do not support multi-party authorisations. Our modelbased approach expresses these differences at a higher level and supports code generation to DAML and Solidity.” (Al-Azzoni et al., p. 2) #ffd400
* *
- “critical security properties must be tested.” (Al-Azzoni et al., p. 2) #ffd400
*Which one? At what level? WHat are the sucurty properties are you referring to? *
- “we generate test scripts including assertions as oracles to run automatically and fail when encountering access control errors.” (Al-Azzoni et al., p. 2) #a28ae5
* *
- “ACPs” (Al-Azzoni et al., p. 2) #ffd400
*What's the execution environmnet you are supporting? What kinds of application can you support? *
- “participant P must authorise action A” (Al-Azzoni et al., p. 2) #a28ae5
* *
- “n members of role R must authorise action A” (Al-Azzoni et al., p. 2) #a28ae5
* *
- “Accepting or rejecting traces are produced by the Groove model checker (Ghamarian et al. 2012) using a start graph and temporal logic formulas derived from the RBACM. Test scripts in DAML are produced based on a test model using a Java EMF application and Acceleo templates” (Al-Azzoni et al., p. 2) #ffd400
*Without exampes it's difficult to grasp the details. Readers is supposed to figure out how this works on his/her own. *
- “Our tests discover design-level faults in access control code. Design-level faults are deviations from the access control requirements expressed in an RBACM, that can arise from implementing (correctly) a faulty model, not from arbitrary implementation errors. This limitation is in line with related work on testing access control policies (Daoudagh et al. 2015; Martin & Xie 2007) which must be complemented by code-based techniques for comprehensive testing.” (Al-Azzoni et al., p. 2) #ffd400
*See my previous comment about the need of examples. *
- “Who can authorise a transaction if a participant is away? or If a given sequence of actions cannot be authorised, can I enable the process by adding a new member to a role? where adding a role member itself requires authorisation.” (Al-Azzoni et al., p. 2) #ffd400
*In addition to these cases, what's the support that authors want to introduce in addition to what existing approaches already permit to do? For instance, appraches for specifying documental workflows, already permit to do so, isn't it? *
- “As a use case, we generate scenarios responding to such questions using OpenAI’s o1-preview and o1-mini to validate them with the Groove model checker, combining the domain knowledge of LLMs with the safety of a formal model.” (Al-Azzoni et al., p. 2) #ffd400
*Here, the use of LLMs appear very suddenly. What's the problem you want to solve that requires automation capabilities based on LLMs? *
- “model-based testing and validation based on domain-specific languages with complex graphlike structure and operational semantics.” (Al-Azzoni et al., p. 2) #a28ae5
* *
- “DLS” (Al-Azzoni et al., p. 2) #ff6666
*-> DSL *
- “validate scenarios suggested by LLMs for testing or helping users at runtime” (Al-Azzoni et al., p. 2) #ffd400
*Maybe this is the answer to my previous question. In any case, it is necessary to introduce the challenges that authors propose to solve by means of LLMs,. The usage of such technologies needs to be justifyed too! *
- “DLS” (Al-Azzoni et al., p. 2) #ff6666
*-> DSL *
- “The innovation in this paper is to use the graphical operational semantics to generated tests from counterexamples to LTL formulas that describe the scenarios to be validated through testing.” (Al-Azzoni et al., p. 3) #a28ae5
* *
- “membership” (Al-Azzoni et al., p. 3) #5fb236
* *
- “authorisation” (Al-Azzoni et al., p. 3) #5fb236
* *
- “The language also supports alternative authorisations indicated by a ∨ (or) symbol within a white square” (Al-Azzoni et al., p. 3) #ffd400
*This not very well explained in the figure. Moreover, Alice is both a submitted and an evaluator? So it means that she is part of the evaluation process for her homework???? *
- “outlined in Fig. 1.” (Al-Azzoni et al., p. 3) #ffd400
*It's not the right reference I guess, which should be instead the listing at pag. 4. *
- “Figure 1 Outline of our approach” (Al-Azzoni et al., p. 3) #ffd400
*The label of the arrow between EMF Test Generator and RBACM Test Model should be generates, isn't it? *
- “GXL” (Al-Azzoni et al., p. 3) #ff6666
*This is not accessible, the reader gets redirected to https://unblock.uni-koblenz.de/redirect/ *
- “template” (Al-Azzoni et al., p. 4) #ffd400
*The template requires explanation for readers that are not expert of DAML *
- “alice : Party bob : Party chris : Party doug : Party emma : Party comments : Text” (Al-Azzoni et al., p. 4) #ffd400
*so this is not done at the metalevel, instead it is required to know the instances of each concept, right? *
- “The effect is that this choice requires the authorisation of Alice in addition to that of Bob or at least two members in the role HWEvaluator_Role as specified by the RBACM.” (Al-Azzoni et al., p. 5) #ffd400
*I would expected to see that HWEaluator should not HWSubmitter. *
- “support the representation of test cases as a basis for code generation.” (Al-Azzoni et al., p. 7) #5fb236
* *
- “This is useful because the system under test may incorrectly require authorisation by a different participant than specified in the model, which corresponds to an incorrect accept trace with that participant added.” (Al-Azzoni et al., p. 7) #5fb236
* *
- “In this section, we discuss the results of a case study involving the use of ChatGPT in generating RBACMs to test our approach and for creating scenarios representing successful executions of workflows with dynamic control access.” (Al-Azzoni et al., p. 7) #ffd400
*IT's not clear what are the motivations supporting the need of such technology. I'm not against it, I'm just wondering what's the issues in using e.g., existing mutation technniques that are able to generate mutations starting from a seed model (see e.g., Wodel).
In other words, what's authors wanted to check/analyze with the generated models? *
- “generate test cases and validate scenarios based on a DSL for multi-party rolebased access control in smart contracts.” (Al-Azzoni et al., p. 12) #ffd400
* *
- “generate and validate access control traces.” (Al-Azzoni et al., p. 12) #ffd400
* *
- “We experimented with chatGPT to generate “realworld” RBACMs in different domains. This approach could be used to generate a set of benchmark models.” (Al-Azzoni et al., p. 12) #ffd400
* *