TY - GEN
T1 - ATLAS
T2 - 25th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2026
AU - Signoles, Julien
AU - Boukir, Khaoula
AU - Nasri, Amine
N1 - Publisher Copyright:
© 2026 Copyright held by the owner/author(s).
PY - 2026/6/23
Y1 - 2026/6/23
N2 - Access control is a classical way to express which users are allowed to do which actions on which objects. Many formalisms study how to model access control policies. However, fewer works target formal verification of an actual implementation with respect to a given policy. This paper presents ATLAS, a new formal specification language for expressing access control policies. This language allows for modeling an access control policy, linking it to a source code, and generating automatically formal annotations in order to verify that a source code correctly implements the modeled policy. This workflow is implemented as a new Frama-C plug-in that generates ACSL annotations, which can be proved by deductive verification or checked at runtime.
AB - Access control is a classical way to express which users are allowed to do which actions on which objects. Many formalisms study how to model access control policies. However, fewer works target formal verification of an actual implementation with respect to a given policy. This paper presents ATLAS, a new formal specification language for expressing access control policies. This language allows for modeling an access control policy, linking it to a source code, and generating automatically formal annotations in order to verify that a source code correctly implements the modeled policy. This workflow is implemented as a new Frama-C plug-in that generates ACSL annotations, which can be proved by deductive verification or checked at runtime.
KW - Access Control
KW - Deductive Verification
KW - Formal Specification Language
KW - Runtime Annotation Checking
UR - https://www.scopus.com/pages/publications/105043833324
U2 - 10.1145/3814885.3816415
DO - 10.1145/3814885.3816415
M3 - Conference contribution
AN - SCOPUS:105043833324
T3 - GPCE 2026 - Proceedings of the 25th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, Co-located with ECOOP 2026
SP - 15
EP - 26
BT - GPCE 2026 - Proceedings of the 25th ACM SIGPLAN International Conference on Generative Programming
A2 - van Binsbergen, L. Thomas
A2 - Struber, Daniel
A2 - Parreaux, Lionel
PB - Association for Computing Machinery, Inc
Y2 - 29 June 2026 through 29 June 2026
ER -