Wang, Zeng and Mathur (QSiC 2012) proposed a security assurance framework that combines formal verification of a Z security-policy specification (via a three-step proof procedure in the Z/EVES theorem prover) with security functional testing generated from the verified specification under a criterion called strict schema coverage, supported by their ZBSAT toolkit. The framework was validated only on the Chinese Wall Model and its Java implementation. The authors' stated open question — whether the approach generalizes to further security policies, their conclusion planning application to more advanced systems such as Z-specified role-based access control (RBAC), and whether it remains feasible and efficient beyond the single case study — has not been taken up by any later work. The problem is to instantiate and evaluate the framework on a Z-specified RBAC policy and an implementation of it, assessing feasibility and scalability in the manner of the original Chinese Wall Model study and improving automation of the verification and test-generation steps.

Background

Security policies such as access control are often written first as formal specifications to remove ambiguity, but two gaps remain: the formal model itself may be incorrect, and the implementation may not conform to it. The paper underlying this candidate (Wang, Zeng and Mathur, QSiC 2012) addresses both gaps in one pipeline. It uses the Z notation — a model-based formal specification language built from typed sets, relations, and schemas, where a schema groups variable declarations with logical predicates defining an operation's preconditions and postconditions — to specify a security policy. Correctness of the specification is then established by formal verification in Z/EVES, a theorem prover for Z, through three integrated steps: a domain check (the schema's declared variables have non-empty domains), an existence/initialization check (an initial state satisfying the state invariant exists), and proofs of the security properties themselves as theorems. Because a verified specification still says nothing about the implementation, the framework then derives security functional tests — tests of the security-relevant behavior of the implementation — directly from the verified Z schemas. The test criterion, strict schema coverage, requires that each condition in an operation's precondition predicates be driven to both true and false in tests where the operation's postcondition outcome (a success schema or one of several numbered failure schemas) is directly correlated with that condition's value; an abstract syntax tree (AST) built from the schema predicates, with quantifiers eliminated, supports mechanical extraction of the test cases. The whole procedure is supported by the ZBSAT toolkit (Z specification Based Security Assurance Toolkit), which drives Z/EVES through a socket interface and automates test generation. The empirical evaluation covered exactly one policy: the Chinese Wall Model (CWM), a commercial-security policy that forbids access to data of companies conflicting with a user's prior accesses, in a study where the 120 generated tests killed all 422 non-equivalent mutants (seeded program faults) of a Java implementation, outperforming random testing. Related lines existed before and after the paper: Hu and Ahn (SACMAT 2008) enabled verification plus conformance testing of access control models, Masood, Ghafoor and Mathur (2010) performed conformance testing of temporal role-based access control, and later model-driven work (e.g., Nguyen et al. 2026 for attribute-based access control) pursues the same assurance goal with other machinery. None of these uses the Z/strict-schema-coverage route, so the question left open by the source paper — whether that route works beyond one case study — remains genuinely unresolved.

Problem Statement

Instantiate and evaluate the security assurance framework of Wang, Zeng and Mathur (2012) on a Z-specified role-based access control (RBAC) policy and an implementation of it, in order to determine whether the framework — verified Z specification, strict-schema-coverage security functional testing, and the ZBSAT toolchain (or a faithful reimplementation, meaning one that implements the same three-step verification formulae and the same strict-schema-coverage AST-based test-derivation procedure, with reproduction of the Chinese Wall Model case results as evidence of faithfulness) — is feasible and scalable beyond the single Chinese Wall Model case study. Concretely, the solver must: (1) take or produce a Z specification of an RBAC policy (core RBAC with user-role and permission-role assignment, role hierarchy, and sessions is the natural scope; existing Z-specified RBAC work in the literature may be used as the base, consistent with the authors' stated plan — as reported in the open-access survey of Kulik et al. (2022) — to apply the framework to Z-specified RBAC); (2) discharge the framework's three verification obligations — domain check, initialization/existence check, and the RBAC security properties as theorems — in Z/EVES or an equivalent Z theorem prover, reporting the proof effort (e.g., number and difficulty of proof steps) in comparison with the CWM study; (3) generate the security functional test suite from the verified schemas under the strict schema coverage criterion, giving a precise instantiation of the criterion's 'direct correlation' between precondition conditions and success/failure outcome schemas for RBAC operations; (4) check conformance of an RBAC implementation (e.g., a Java implementation, as in the CWM study) with the generated tests, and evaluate fault-detection effectiveness by mutation testing against at least one baseline such as random testing, mirroring the CWM evaluation, whose own mutation-test comparison was the paper's demonstration of the criterion's efficiency; and (5) report where the framework's formulae, criterion, or tooling needed modification or further automation (reduction of manual proof and test-generation effort) to handle the larger and structurally different RBAC specification. The feasibility and scalability question is settled either by a working generalization of the framework or by a rigorous negative result demonstrating precisely where and why the framework fails to scale or the criterion cannot be instantiated for RBAC.

References

  1. Weiguang Wang, Qingkai Zeng, Aditya P. Mathur (2012). A Security Assurance Framework Combining Formal Verification and Security Functional Testing. In: 2012 12th International Conference on Quality Software (QSiC), pp. 136–139. DOI: 10.1109/QSiC.2012.34. https://doi.org/10.1109/QSiC.2012.34
  2. Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter W. V. Tran-Jørgensen, James Woodcock (2022). A Survey of Practical Formal Methods for Security. Formal Aspects of Computing 34(1): 1–39. DOI: 10.1145/3522582. https://doi.org/10.1145/3522582 (open-access preprint: arXiv:2109.01362)
  3. Michael Felderer, Philipp Zech, Ruth Breu, Matthias Büchler, Alexander Pretschner (2016). Model-based security testing: a taxonomy and systematic classification. Software Testing, Verification and Reliability 26(2): 119–148. DOI: 10.1002/stvr.1580. https://doi.org/10.1002/stvr.1580
  4. Hassan Saeed, Imran Shafi, Jamil Ahmad, Adnan Ahmed Khan, Tahir Khurshaid, Imran Ashraf (2025). Review of Techniques for Integrating Security in Software Development Lifecycle. Computers, Materials & Continua 82(1): 139–172. DOI: 10.32604/cmc.2024.057587. https://doi.org/10.32604/cmc.2024.057587
  5. Mark Fischer, Fabian Langer, Johannes Mono, Clemens Nasenberg, Nils Albartus (2021). Hardware Penetration Testing Knocks Your SoCs Off. IEEE Design & Test 38(1): 14–21. DOI: 10.1109/MDAT.2020.3013730. https://doi.org/10.1109/MDAT.2020.3013730
  6. Gabriel Pedroza (2013). Assisting the Design of Secured Applications for Embedded Systems (Conception Assistée des Logiciels Sécurisés pour les Systèmes Embarqués). Doctoral thesis. https://dblp.org/rec/phd/hal/Pedroza13.html
  7. Matthias Büchler (2015). Semi-Automatic Security Testing of Web Applications with Fault Models and Properties. Doctoral thesis, TU München. https://dblp.org/rec/phd/dnb/Buchler15.html
  8. Hongxin Hu, Gail-Joon Ahn (2008). Enabling verification and conformance testing for access control model. In: Proceedings of the 13th ACM Symposium on Access Control Models and Technologies (SACMAT), pp. 195–204. DOI: 10.1145/1377836.1377867. https://doi.org/10.1145/1377836.1377867
  9. Ammar Masood, Arif Ghafoor, Aditya P. Mathur (2010). Conformance Testing of Temporal Role-Based Access Control Systems. IEEE Transactions on Dependable and Secure Computing 7(2): 144–158. DOI: 10.1109/TDSC.2008.41. https://doi.org/10.1109/TDSC.2008.41
  10. Mark Slaymaker, David Power, Andrew Simpson (2010). Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods. In: Abstract State Machines, Alloy, B and Z (ABZ 2010), Lecture Notes in Computer Science, pp. 349–362. DOI: 10.1007/978-3-642-11811-1_26. https://doi.org/10.1007/978-3-642-11811-1_26
  11. Jingda Yang, Sudhanshu Arya, Ying Wang (2024). Formal-Guided Fuzz Testing: Targeting Security Assurance From Specification to Implementation for 5G and Beyond. IEEE Access 12: 29175–29193. DOI: 10.1109/ACCESS.2024.3369613. https://doi.org/10.1109/ACCESS.2024.3369613
  12. Duc-Hieu Nguyen, Yuichi Sei, Yasuyuki Tahara, Akihiko Ohsuga (2026). Model-driven approach enabling formalization and conformance testing of attribute-based access control policies for business processes. Journal of Computer Security 34(4): 261–300. DOI: 10.1177/0926227X261421496. https://doi.org/10.1177/0926227X261421496