×

zbMATH — the first resource for mathematics

Automatic inference of access permissions. (English) Zbl 1326.68092
Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 202-218 (2012).
Summary: 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.
For the entire collection see [Zbl 1236.68007].
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL 2005. ACM (2005) · Zbl 1369.68130 · doi:10.1145/1040305.1040327
[2] Boyland, J.: Checking Interference with Fractional Permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003) · Zbl 1067.68537 · doi:10.1007/3-540-44898-5_4
[3] Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009. ACM (2009) · Zbl 1315.68085 · doi:10.1145/1594834.1480917
[4] Calcagno, C., Distefano, D., Vafeiadis, V.: Bi-abductive Resource Invariant Synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 259–274. Springer, Heidelberg (2009) · Zbl 05641685 · doi:10.1007/978-3-642-10672-9_19
[5] Cataño, N., Huisman, M.: CHASE: A Static Checker for JML’s Assignable Clause. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 26–40. Springer, Heidelberg (2002) · Zbl 1022.68576 · doi:10.1007/3-540-36384-X_6
[6] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977. ACM (1977) · Zbl 1149.68389 · doi:10.1145/512950.512973
[7] Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979. ACM (1979) · Zbl 1323.68356 · doi:10.1145/567752.567778
[8] Dantzig, G.B.: Linear programming and extensions. Rand Corporation Research Study. Princeton Univ. Press (1963) · doi:10.1515/9781400884179
[9] Ernst, M.D., Perkins, J.H., Guo, P.J., Mccamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69, 35–45 (2007) · Zbl 1161.68390 · doi:10.1016/j.scico.2007.01.015
[10] Ferrara, P.: A fast and precise analysis for data race detection. In: Bytecode (2008)
[11] Flanagan, C., Leino, K.R.M.: Houdini, an Annotation Assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001) · Zbl 0977.68671 · doi:10.1007/3-540-45251-6_29
[12] Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011) · Zbl 05930518 · doi:10.1007/978-3-642-20398-5_4
[13] Leino, K.R.M., Logozzo, F.: Loop Invariants on Demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119–134. Springer, Heidelberg (2005) · Zbl 1159.68374 · doi:10.1007/11575467_9
[14] Leino, K.R.M., Müller, P.: A Basis for Verifying Multi-threaded Programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009) · Zbl 1234.68078 · doi:10.1007/978-3-642-00590-9_27
[15] Leino, K.R.M., Müller, P., Smans, J.: Verification of Concurrent Programs with Chalice. In: FOSAD 2009. LNCS, vol. 5705, pp. 195–222. Springer, Heidelberg (2009)
[16] Lev-Ami, T., Sagiv, M.: TVLA: A System for Implementing Static Analyses. In: SAS 2000. LNCS, vol. 1824, pp. 280–302. Springer, Heidelberg (2000) · Zbl 0966.68580 · doi:10.1007/978-3-540-45099-3_15
[17] Fähndrich, M., Logozzo, F.: Static Contract Checking with Abstract Interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011) · Zbl 1308.68033 · doi:10.1007/978-3-642-18070-5_2
[18] Mauborgne, L., Rival, X.: Trace Partitioning in Abstract Interpretation Based Static Analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005) · Zbl 1108.68427 · doi:10.1007/978-3-540-31987-0_2
[19] Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19, 279–285 (1976) · Zbl 0322.68010 · doi:10.1145/360051.360224
[20] Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL 2005. ACM (2005) · Zbl 1369.68151 · doi:10.1145/1040305.1040326
[21] Rakamaric, Z., Hu, A.J.: Automatic inference of frame axioms using static analysis. In: ASE 2008. IEEE (2008) · doi:10.1109/ASE.2008.19
[22] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE Computer Society (2002) · doi:10.1109/LICS.2002.1029817
[23] Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM ToPLaS 24(3), 217–298 (2002) · Zbl 05459332 · doi:10.1145/514188.514190
[24] Smans, J., Jacobs, B., Piessens, F.: VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 220–239. Springer, Heidelberg (2008) · Zbl 05288318 · doi:10.1007/978-3-540-68863-1_14
[25] Smans, J., Jacobs, B., Piessens, F.: Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 148–172. Springer, Heidelberg (2009) · Zbl 05596255 · doi:10.1007/978-3-642-03013-0_8
[26] Spoto, F., Poll, E.: Static analysis for JML’s assignable clauses. In: FOOL 2003 (2003)
[27] Yasuoka, H., Terauchi, T.: Polymorphic Fractional Capabilities. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 36–51. Springer, Heidelberg (2009) · Zbl 1248.68157 · doi:10.1007/978-3-642-03237-0_5
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.