P. Ferrara and P. Müller.
Automatic inference of access permissions

In Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012), LNCS, Springer, Philadelphia, USA, January 22-24, 2012

Final version: Pdf (400 KB)
Slides: Pdf (392 KB)

Abstract: Access permissions are used in several program verification approaches such as those based on separation logic or implicit dynamic frames to simplify framing and to provide a basis for reasoning about concurrent code. However, access permissions increase the annotation overhead because programmers need to specify for each program component which permissions it requires or provides. We present a new static analysis based on abstract interpretation to infer access permissions automatically. Our analysis computes a symbolic approximation of the permissions owned for each heap location at each program point and infers a constraint system over these symbolic permissions that reflects the permission requirements of each heap access in the program. The constraint system is solved using linear programming. Our analysis is parametric in the permission system and supports, for instance, fractional and counting permissions. Experimental results demonstrate that our analysis is fast and is able to infer almost all access permissions for our case studies.

Keywords: Abstract interpretation, Static analysis, Frame information, Access permissions

Bibtex:

@inproceedings{FM12,
  author = {Ferrara, Pietro and Müller, Peter},
  title = {Automatic inference of access permissions},
  booktitle = {Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012)},
  year = {2012},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  month = {January},
}