John Tang Boyland
ABSTRACT
The concept of controlling access to mutable shared data via permissions is at the heart of permission logics such as separation logic and implicit dynamic frames, and is also used in type systems, for instance, to give a semantics to "read-only" annotations. Existing permission models have different strengths in terms of expressiveness. Fractional permissions, for example, enable unbounded (recursive) splitting, whereas counting permissions enable unbounded subtraction of the same permission amount. Combining these strengths in a single permission model appeared to increase the complexity for the user and tools. In this paper we extend our previous work on abstract read permissions by providing them with a novel constraint semantics, which retains the use of the domain of rational numbers but enables unbounded subtraction of identical amounts. Thus we can keep an intuitive model conducive to SMT solvers while enabling "counting."
- R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in separation logic. In POPL, pages 259--270. ACM, 2005. Google Scholar
Digital Library
- J. Boyland. Checking interference with fractional permissions. In SAS, volume 2694 of LNCS, pages 55--72. Springer, 2003. Google ScholarDigital Library
- J. Boyland. Fractional permissions. In Aliasing in Object-Oriented Programming, volume 7850 of LNCS, pages 270--288. Springer, 2013. Google ScholarDigital Library
- R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In APLAS, volume 5904 of LNCS, pages 161--177. Springer, 2009. Google ScholarDigital Library
- S. Heule, K. R. M. Leino, P. Müller, and A. J. Summers. Abstract read permissions: Fractional permissions without the fractions. In VMCAI, volume 7737 of LNCS, pages 315--334. Springer, 2013.Google Scholar
- B. Jacobs and F. Piessens. The VeriFast program verifier. Technical Report CW-520, KU Leuven, Aug. 2008.Google Scholar
- U. Juhasz, I. T. Kassios, P. Müller, M. Novacek, M. Schwerhoff, and A. J. Summers. Viper: A verification infrastructure for permission-based reasoning. Technical report, ETH Zurich, 2014.Google Scholar
- X. B. Le, C. Gherghina, and A. Hobor. Decision procedures over sophisticated fractional permissions. In APLAS, volume 7705 of LNCS, pages 368--385. Springer, 2012.Google Scholar
- K. R. M. Leino and R. Monahan. Reasoning about comprehensions with first-order SMT solvers. In SAC, pages 615--622. ACM, 2009. Google ScholarDigital Library
- K. R. M. Leino and P. Müller. A basis for verifying multi-threaded programs. In ESOP, volume 5502 of LNCS, pages 378--393. Springer, 2009. Google ScholarDigital Library
- M. J. Parkinson and G. M. Bierman. Separation logic and abstraction. In POPL, pages 247--258. ACM, 2005. Google ScholarDigital Library
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74. IEEE, 2002. Google ScholarDigital Library
- J. Smans, B. Jacobs, and F. Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In ECOOP, volume 5653 of LNCS, pages 148--172. Springer, 2009. Google ScholarDigital Library
Index Terms
- Constraint Semantics for Abstract Read Permissions
Recommendations
A flexible role-based delegation model using characteristics of permissions
DEXA'05: Proceedings of the 16th international conference on Database and Expert Systems ApplicationsRole-Based Access Control(RBAC) has recently received considerable attention as a promising alternative to traditional discretionary and mandatory access controls.[7] RBAC ensures that only authorized users are given access to protected data or ...
Abstract Read Permissions: Fractional Permissions without the Fractions
VMCAI 2013: Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 7737Fractional Permissions are a popular approach to reasoning about programs that use shared-memory concurrency, because they provide a way of proving data race freedom while permitting concurrent read access. However, specification using fractional ...
Program synthesis in administration of higher-order permissions
SACMAT '11: Proceedings of the 16th ACM symposium on Access control models and technologiesIn "administrative" access control, policy controls permissions not just on application actions, but also on actions to modify permissions, on actions to modify permissions on those actions, and so on. One context of work in administrative policy is "...
Comments