Secure the Clones
Thomas Jensen (INRIA Rennes), Florent Kirchner (INRIA Rennes), David, Pichardie (INRIA Rennes)

TL;DR
This paper introduces a type-based annotation system for secure, modular object cloning in Java, ensuring deep copies and preventing malicious subclassing through static enforcement and formal proof.
Contribution
It proposes a novel static enforcement mechanism for copy policies in Java, supported by a formal proof of correctness in Coq, enhancing security in object cloning.
Findings
Effective static enforcement of copy policies
Formal proof of correctness in Coq
Successful implementation on Java libraries
Abstract
Exchanging mutable data objects with untrusted code is a delicate matter because of the risk of creating a data space that is accessible by an attacker. Consequently, secure programming guidelines for Java stress the importance of using defensive copying before accepting or handing out references to an internal mutable object. However, implementation of a copy method (like clone()) is entirely left to the programmer. It may not provide a sufficiently deep copy of an object and is subject to overriding by a malicious sub-class. Currently no language-based mechanism supports secure object cloning. This paper proposes a type-based annotation system for defining modular copy policies for class-based object-oriented programs. A copy policy specifies the maximally allowed sharing between an object and its clone. We present a static enforcement mechanism that will guarantee that all classes…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
