Verifying access control properties with design by contract: Framework and lessons learned

Carlos E. Rubio-Medrano, Gail-Joon Ahn, Karsten Sohr

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

1 Citation (Scopus)

Abstract

Ensuring the correctness of high-level security properties including access control policies in mission-critical applications is indispensable. Recent literature has shown how immaturity of such properties has caused serious security vulnerabilities, which are likely to be exploited by malicious parties for compromising a given application. This situation gets aggravated by the fact that modern applications are mostly built on previously developed reusable software modules and any failures in security properties in these reusable modules may lead to vulnerabilities across associated applications. In this paper, we propose a framework to address this issue by adopting Design by Contract (DBC) features. Our framework accommodates security properties in each application focusing on access control requirements. We demonstrate how access control requirements based on ANSI RBAC standard model can be specified and verified at the source code level.

Original languageEnglish (US)
Title of host publicationProceedings - International Computer Software and Applications Conference
Pages21-26
Number of pages6
DOIs
StatePublished - 2013
Event2013 IEEE 27th International Parallel and Distributed Processing Symposium Workshops and PhD Forum, IPDPSW 2013 - Boston, MA, United States
Duration: May 20 2013May 24 2013

Other

Other2013 IEEE 27th International Parallel and Distributed Processing Symposium Workshops and PhD Forum, IPDPSW 2013
CountryUnited States
CityBoston, MA
Period5/20/135/24/13

Fingerprint

Access control

Keywords

  • Access control
  • Formal verification
  • Security

ASJC Scopus subject areas

  • Software
  • Computer Science Applications

Cite this

Rubio-Medrano, C. E., Ahn, G-J., & Sohr, K. (2013). Verifying access control properties with design by contract: Framework and lessons learned. In Proceedings - International Computer Software and Applications Conference (pp. 21-26). [6649794] https://doi.org/10.1109/COMPSAC.2013.7

Verifying access control properties with design by contract : Framework and lessons learned. / Rubio-Medrano, Carlos E.; Ahn, Gail-Joon; Sohr, Karsten.

Proceedings - International Computer Software and Applications Conference. 2013. p. 21-26 6649794.

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

Rubio-Medrano, CE, Ahn, G-J & Sohr, K 2013, Verifying access control properties with design by contract: Framework and lessons learned. in Proceedings - International Computer Software and Applications Conference., 6649794, pp. 21-26, 2013 IEEE 27th International Parallel and Distributed Processing Symposium Workshops and PhD Forum, IPDPSW 2013, Boston, MA, United States, 5/20/13. https://doi.org/10.1109/COMPSAC.2013.7
Rubio-Medrano CE, Ahn G-J, Sohr K. Verifying access control properties with design by contract: Framework and lessons learned. In Proceedings - International Computer Software and Applications Conference. 2013. p. 21-26. 6649794 https://doi.org/10.1109/COMPSAC.2013.7
Rubio-Medrano, Carlos E. ; Ahn, Gail-Joon ; Sohr, Karsten. / Verifying access control properties with design by contract : Framework and lessons learned. Proceedings - International Computer Software and Applications Conference. 2013. pp. 21-26
@inproceedings{c38d40fd7a034305bb1af8520bafbbb9,
title = "Verifying access control properties with design by contract: Framework and lessons learned",
abstract = "Ensuring the correctness of high-level security properties including access control policies in mission-critical applications is indispensable. Recent literature has shown how immaturity of such properties has caused serious security vulnerabilities, which are likely to be exploited by malicious parties for compromising a given application. This situation gets aggravated by the fact that modern applications are mostly built on previously developed reusable software modules and any failures in security properties in these reusable modules may lead to vulnerabilities across associated applications. In this paper, we propose a framework to address this issue by adopting Design by Contract (DBC) features. Our framework accommodates security properties in each application focusing on access control requirements. We demonstrate how access control requirements based on ANSI RBAC standard model can be specified and verified at the source code level.",
keywords = "Access control, Formal verification, Security",
author = "Rubio-Medrano, {Carlos E.} and Gail-Joon Ahn and Karsten Sohr",
year = "2013",
doi = "10.1109/COMPSAC.2013.7",
language = "English (US)",
pages = "21--26",
booktitle = "Proceedings - International Computer Software and Applications Conference",

}

TY - GEN

T1 - Verifying access control properties with design by contract

T2 - Framework and lessons learned

AU - Rubio-Medrano, Carlos E.

AU - Ahn, Gail-Joon

AU - Sohr, Karsten

PY - 2013

Y1 - 2013

N2 - Ensuring the correctness of high-level security properties including access control policies in mission-critical applications is indispensable. Recent literature has shown how immaturity of such properties has caused serious security vulnerabilities, which are likely to be exploited by malicious parties for compromising a given application. This situation gets aggravated by the fact that modern applications are mostly built on previously developed reusable software modules and any failures in security properties in these reusable modules may lead to vulnerabilities across associated applications. In this paper, we propose a framework to address this issue by adopting Design by Contract (DBC) features. Our framework accommodates security properties in each application focusing on access control requirements. We demonstrate how access control requirements based on ANSI RBAC standard model can be specified and verified at the source code level.

AB - Ensuring the correctness of high-level security properties including access control policies in mission-critical applications is indispensable. Recent literature has shown how immaturity of such properties has caused serious security vulnerabilities, which are likely to be exploited by malicious parties for compromising a given application. This situation gets aggravated by the fact that modern applications are mostly built on previously developed reusable software modules and any failures in security properties in these reusable modules may lead to vulnerabilities across associated applications. In this paper, we propose a framework to address this issue by adopting Design by Contract (DBC) features. Our framework accommodates security properties in each application focusing on access control requirements. We demonstrate how access control requirements based on ANSI RBAC standard model can be specified and verified at the source code level.

KW - Access control

KW - Formal verification

KW - Security

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

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

U2 - 10.1109/COMPSAC.2013.7

DO - 10.1109/COMPSAC.2013.7

M3 - Conference contribution

AN - SCOPUS:84891312893

SP - 21

EP - 26

BT - Proceedings - International Computer Software and Applications Conference

ER -