Email Gateway (Aug 18 2022 at 17:30): Email Gateway (Aug 18 2022 at 17:30):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
it is a pleasure to present two papers for the research field "Test&Proof",
aiming at novel combinations of (Isabelle)-proofs and test-generation techniques.
A) Authors: A. Brucker, L. Brügger, P. Kearney and Burkhart Wolff:
Title: Verified Firewall Policy Transformations for Test Case Generation
Abstract:
We present an optimization technique for model-based generation of test cases
for firewalls. Based on a formal model for firewall policies in higher-order logic,
we derive a collection of semantics-preserving policy transformation rules and an
algorithm that optimizes the specification with respect of the number of test
cases required for path coverage. The correctness of the rules and the algorithm
is established by formal proofs in Isabelle/HOL. Finally, we use the normalized
policies to generate test cases with the domain-specific firewall testing tool
Isabelle/TestGen/FW.
The resulting procedure is characterized by a gain in efficiency
of two orders of magnitude and can handle configurations with
hundreds of rules as occur in practice.
Appeared in ICST 2010, URL: .pdf
B) Authors: A. Brucker, L. Brügger, P. Kearney, and B. Wolff.
Title: An approach to modular and testable security models of real-world health-care applications.
Abstract: We present a generic modular policy modelling framework and instantiate it with a
substantial case study for model- based testing of some key security mechanisms of applica- tions and services
of the NPfIT. NPfIT, the National Pro- gramme for IT, is a very large-scale development project aiming to modernise
the IT infrastructure of the National Health Service (NHS) in England. Consisting of heteroge- neous and distributed
applications, it is an ideal target for model-based testing techniques of a large system exhibiting critical security features.
We model the four information governance principles, com- prising a role-based access control model, as well as policy
rules governing the concepts of patient consent, sealed en- velopes and legitimate relationships. The model is given in
Higher-order Logic (HOL) and processed together with suit- able test specifications in the hol-TestGen system, that
generates test sequences according to them. Particular em- phasis is put on the modular description of security policies
and their generic combination and its consequences for model-based testing.
To appear in SACMATR 2011, URL: http://www.lri.fr/~wolff/papers/conf/2011-sacmat-mbtsec-npfit.pdf
Enjoy !
bu
Last updated: Apr 26 2024 at 16:20 UTC