Abstract
Detecting programming errors and vulnerabilities in software is increasingly important, and building tools that help developers with this task is a crucial area of investigation on which the industry depends. In object-oriented languages, one naturally defines stateful objects where the safe use of methods depends on their internal state; the correct use of objects according to their protocols is then enforced at compile-time by an analysis based on behavioral types.
We present Java Typestate Checker (JATYC), a tool based on the Checker Framework that verifies Java programs with respect to typestates. These define the object’s states, the methods that can be called in each state, and the states resulting from the calls. The tool offers the following strong guarantees: sequences of method calls obey to object’s protocols; completion of objects’ protocols; detection of null-pointer exceptions; and control of the sharing of resources through access permissions.
To the best of our knowledge, there are no research or industrial tools that offer all these features. In particular, the implementation of sharing control in a typestate-based tool seems to be novel, and has an important impact on programming flexibility, since, for most programs, the linear discipline imposed by behavioral types is too strict.
Sharing of objects is enabled by means of an assertion language incorporating fractional permissions; to lift from programmers the burden of writing the assertions, JATYC infers all of these by building a constraint system and solving it with Z3, producing general assertions sufficient to accept the code, if these exist.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The second to last release was on 2019: https://jastadd.cs.lth.se/releases/jastadd2/2.3.4/release-notes.php.
- 2.
- 3.
- 4.
- 5.
- 6.
- 7.
- 8.
An example is available at https://tinyurl.com/2hmwx7vk.
- 9.
The class could be a subclass of the abstract class java.io.Reader.
- 10.
Code examples are available online at https://git.io/JtR7E.
- 11.
The complete grammar is available at https://git.io/JtMu3.
- 12.
Example of droppable states at https://git.io/JOqfc.
- 13.
The fact that null is a value of any type is the source of Java not being type safe [1].
References
Amin, N., Tate, R.: Java and Scala’s type systems are unsound: the existential crisis of null pointers. ACM SIGPLAN Notices 51(10), 838–848 (2016). https://doi.org/10.1145/3022671.2984004
Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2–3), 95–230 (2016). https://doi.org/10.1561/2500000031
Bacchiani, L., Bravetti, M., Lange, J., Zavattaro, G.: A session subtyping tool, to appear. In: 23rd International Conference on Coordination Models and Languages (2021)
Beckman, N.E., Kim, D., Aldrich, J.: An empirical study of object protocols in the wild. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 2–26. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22655-7_2
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 259–270 (2005). https://doi.org/10.1145/1040305.1040327
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44898-5_4
Bravetti, M., et al.: Behavioural types for memory and method safety in a core object-oriented language. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 105–124. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-64437-6_6
Cardelli, L.: Type systems. ACM Comput. Surv. 28(1), 263–264 (1996). https://doi.org/10.1145/234313.234418
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
DeLine, R., Fähndrich, M.: The fugue protocol checker: Is your software baroque. Technical Report, Technical Report MSR-TR-2004-07, Microsoft Research (2004)
Dietl, W., Dietzel, S., Ernst, M.D., Muşlu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: The 33rd International Conference on Software Engineering, pp. 681–690 (2011). https://doi.org/10.1145/1985793.1985889
Ekman, T., Hedin, G.: Rewritable reference attributed grammars. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 147–171. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24851-4_7
Ekman, T., Hedin, G.: The jastadd extensible java compiler. In: The 22nd Annual ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications, pp. 1–18 (2007). https://doi.org/10.1145/1297105.1297029
Ferrara, P., Müller, P.: Automatic inference of access permissions. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 202–218. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_14
Garcia, R., Tanter, É., Wolff, R., Aldrich, J.: Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. (TOPLAS) 36(4), 12 (2014). https://doi.org/10.1145/2629609
Girard, J.Y.: Linear logic. Theoretical Comput. Sci. 50(1), 1–101 (1987). https://doi.org/10.1016/0304-3975(87)90045-4
Group, T.P.: The plaid programming language - introduction. https://www.cs.cmu.edu/aldrich/plaid/plaid-intro.pdf. Accessed 10 Apr 2021
Hoare, T.: Null references: The billion dollar mistake, Presentation at QCon London (2009). https://tinyurl.com/eyipowm4
Hüttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. (CSUR) 49(1), 1–36 (2016). https://doi.org/10.1145/2873052
Ishtiaq, S.S., O’hearn, P.W.: Bi as an assertion language for mutable data structures. In: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 14–26 (2001). https://doi.org/10.1145/1988042.1988050
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). https://doi.org/10.1007/978-3-642-20398-5_4
Jemerov, D., Isakova, S.: Kotlin in Action. Manning Publications Company, New York (2017)
Jones, C.B.: Specification and design of (parallel) programs. In: Mason, R.E.A. (ed.) The IFIP 9th World Computer Congress Information Processing, Paris, vol. 83, pp. 321–332 (1983). North-Holland/IFIP (1983)
Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with mungo and stmungo. In: The 18th International Symposium on Principles and Practice of Declarative Programming, pp. 146–159. ACM (2016). https://doi.org/10.1145/2967973.2968595
Mota, J.: Coping with the reality: adding crucial features to a typestate-oriented language. Master’s thesis, NOVA School of Science and Technology (2021). https://github.com/jdmota/java-typestate-checker/blob/master/docs/msc-thesis.pdf
Naden, K., Bocchino, R., Aldrich, J., Bierhoff, K.: A type system for borrowing permissions. ACM SIGPLAN Notices 47(1), 557–570 (2012). https://doi.org/10.1145/2103621.2103722
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_1
Papi, M.M., Ali, M., Correa Jr, T.L., Perkins, J.H., Ernst, M.D.: Practical pluggable types for java. In: The 2008 International Symposium on Software Testing and Analysis, pp. 201–212 (2008). https://doi.org/10.1145/1390630.1390656
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 (2002). https://doi.org/10.1109/lics.2002.1029817
Sadiq, A., Li, Y.F., Ling, S.: A survey on the use of access permission-based specifications for program verification. J. Syst. Softw. 159, 110150 (2020). https://doi.org/10.1016/j.jss.2019.110450
Sunshine, J.: Protocol programmability. Ph.D. thesis, Carnegie Mellon University, Pittsburgh (2013)
Sunshine, J., Naden, K., Stork, S., Aldrich, J., Tanter, É.: First-class state change in plaid. ACM SIGPLAN Notices 46(10), 713–732 (2011). https://doi.org/10.1145/2076021.2048122
Wetsman, N.: Contact tracing app for England and wales failed to flag people exposed to Covid-19. The Verge (2020). https://www.theverge.com/2020/11/2/21546618/uk-coronavirus-contact-tracing-app-error-alert-isolation
Acknowledgements
We warmly acknowledge the anonymous reviewers whose comments and suggestions pushed us to present a more complete and well-rounded discussion of the topics.
This work was partially supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No. 778233 (BehAPI) and by NOVA LINCS (UIDB/04516/2020) via the Portuguese Fundação para a Ciência e a Tecnologia.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 IFIP International Federation for Information Processing
About this paper
Cite this paper
Mota, J., Giunti, M., Ravara, A. (2021). Java Typestate Checker. In: Damiani, F., Dardha, O. (eds) Coordination Models and Languages. COORDINATION 2021. Lecture Notes in Computer Science(), vol 12717. Springer, Cham. https://doi.org/10.1007/978-3-030-78142-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-78142-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-78141-5
Online ISBN: 978-3-030-78142-2
eBook Packages: Computer ScienceComputer Science (R0)
