2026-07-20T05:38:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6103 2024-03-06T10:37:59Z ddc:004 open_access

LJGS: Gradual Security Types for Object-Oriented Languages Fennell, Luminous Thiemann, Peter gradual typing security typing Java hybrid information flow control LJGS is a lightweight Java core calculus with a gradual security type system. The calculus guarantees secure information flow for sequential, class-based, typed object-oriented programming with mutable objects and virtual method calls. An LJGS program is composed of fragments that are checked either statically or dynamically. Statically checked fragments adhere to a security type system so that they incur no run-time penalty whereas dynamically checked fragments rely on run-time security labels. The programmer marks the boundaries between static and dynamic checking with casts so that it is always clear whether a program fragment requires run-time checks. LJGS requires security annotations on fields and methods. A field annotation either specifies a fixed static security level or it prescribes dynamic checking. A method annotation specifies a constrained polymorphic security signature. The types of local variables in method bodies are analyzed flow-sensitively and require no annotation. The dynamic checking of fields relies on a static points-to analysis to approximate implicit flows. We prove type soundness and non-interference for LJGS. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Luminous Fennell and Peter Thiemann 2016 Is Part Of LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2016.9 urn:nbn:de:0030-drops-61031 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.9 eng https://creativecommons.org/licenses/by/3.0/legalcode