Enabling Verification and conformance testing for access control model

Hongxin Hu, Gail-Joon Ahn

Research output: Chapter in Book/Report/Conference proceedingConference contribution

56 Citations (Scopus)

Abstract

Verification and testing are the important step for software assurance. However, such crucial and yet challenging tasks have not been widely adopted in building access control systems. In this paper we propose a methodology to support automatic analysis and conformance testing for access control systems, integrating those features to Assurance Management Framework (AMF). Our methodology attempts to verify formal specifications of a role-based access control model and corresponding policies with selected security properties. Also, we systematically articulate testing cases from formal specifications and validate conformance to the system design and implementation using those cases. In addition, we demonstrate feasibility and effectiveness of our methodology using SAT and Alloy toolset.

Original languageEnglish (US)
Title of host publicationProceedings of ACM Symposium on Access Control Models and Technologies, SACMAT
Pages195-204
Number of pages10
DOIs
StatePublished - 2008
Externally publishedYes
Event13th ACM Symposium on Access Control Models and Technologies, SACMAT'08 - Estes Park, CO, United States
Duration: Jun 11 2008Jun 13 2008

Other

Other13th ACM Symposium on Access Control Models and Technologies, SACMAT'08
CountryUnited States
CityEstes Park, CO
Period6/11/086/13/08

Fingerprint

Access control
Testing
Control systems
Systems analysis
Formal specification

Keywords

  • Access control
  • Alloy
  • Model-based testing
  • Model-based verification
  • Sat solver

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications
  • Safety, Risk, Reliability and Quality
  • Information Systems

Cite this

Hu, H., & Ahn, G-J. (2008). Enabling Verification and conformance testing for access control model. In Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT (pp. 195-204). [1377867] https://doi.org/10.1145/1377836.1377867

Enabling Verification and conformance testing for access control model. / Hu, Hongxin; Ahn, Gail-Joon.

Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT. 2008. p. 195-204 1377867.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Hu, H & Ahn, G-J 2008, Enabling Verification and conformance testing for access control model. in Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT., 1377867, pp. 195-204, 13th ACM Symposium on Access Control Models and Technologies, SACMAT'08, Estes Park, CO, United States, 6/11/08. https://doi.org/10.1145/1377836.1377867
Hu H, Ahn G-J. Enabling Verification and conformance testing for access control model. In Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT. 2008. p. 195-204. 1377867 https://doi.org/10.1145/1377836.1377867
Hu, Hongxin ; Ahn, Gail-Joon. / Enabling Verification and conformance testing for access control model. Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT. 2008. pp. 195-204
@inproceedings{a538c98e610247bd92fa74254117f6fd,
title = "Enabling Verification and conformance testing for access control model",
abstract = "Verification and testing are the important step for software assurance. However, such crucial and yet challenging tasks have not been widely adopted in building access control systems. In this paper we propose a methodology to support automatic analysis and conformance testing for access control systems, integrating those features to Assurance Management Framework (AMF). Our methodology attempts to verify formal specifications of a role-based access control model and corresponding policies with selected security properties. Also, we systematically articulate testing cases from formal specifications and validate conformance to the system design and implementation using those cases. In addition, we demonstrate feasibility and effectiveness of our methodology using SAT and Alloy toolset.",
keywords = "Access control, Alloy, Model-based testing, Model-based verification, Sat solver",
author = "Hongxin Hu and Gail-Joon Ahn",
year = "2008",
doi = "10.1145/1377836.1377867",
language = "English (US)",
isbn = "9781605581293",
pages = "195--204",
booktitle = "Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT",

}

TY - GEN

T1 - Enabling Verification and conformance testing for access control model

AU - Hu, Hongxin

AU - Ahn, Gail-Joon

PY - 2008

Y1 - 2008

N2 - Verification and testing are the important step for software assurance. However, such crucial and yet challenging tasks have not been widely adopted in building access control systems. In this paper we propose a methodology to support automatic analysis and conformance testing for access control systems, integrating those features to Assurance Management Framework (AMF). Our methodology attempts to verify formal specifications of a role-based access control model and corresponding policies with selected security properties. Also, we systematically articulate testing cases from formal specifications and validate conformance to the system design and implementation using those cases. In addition, we demonstrate feasibility and effectiveness of our methodology using SAT and Alloy toolset.

AB - Verification and testing are the important step for software assurance. However, such crucial and yet challenging tasks have not been widely adopted in building access control systems. In this paper we propose a methodology to support automatic analysis and conformance testing for access control systems, integrating those features to Assurance Management Framework (AMF). Our methodology attempts to verify formal specifications of a role-based access control model and corresponding policies with selected security properties. Also, we systematically articulate testing cases from formal specifications and validate conformance to the system design and implementation using those cases. In addition, we demonstrate feasibility and effectiveness of our methodology using SAT and Alloy toolset.

KW - Access control

KW - Alloy

KW - Model-based testing

KW - Model-based verification

KW - Sat solver

UR - http://www.scopus.com/inward/record.url?scp=57349119890&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=57349119890&partnerID=8YFLogxK

U2 - 10.1145/1377836.1377867

DO - 10.1145/1377836.1377867

M3 - Conference contribution

SN - 9781605581293

SP - 195

EP - 204

BT - Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT

ER -