Skip to Main content Skip to Navigation
New interface
Conference papers

Program Transformation for Non-interference Verification on Programs with Pointers

Mounir Assaf 1, 2 Julien Signoles 1 Frédéric Tronel 2 Eric Totel 2 
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
2 CIDRE - Confidentialité, Intégrité, Disponibilité et Répartition
CentraleSupélec, Inria Rennes – Bretagne Atlantique , IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
Abstract : Novel approaches for dynamic information flow monitoring are promising since they enable permissive (accepting a large subset of executions) yet sound (rejecting all insecure executions) enforcement of non-interference. In this paper, we present a dynamic information flow monitor for a language supporting pointers. Our flow-sensitive monitor relies on prior static analysis in order to soundly enforce non-interference. We also propose a program transformation that preserves the behavior of initial programs and soundly inlines our security monitor. This program transformation enables both dynamic and static verification of non-interference.
Document type :
Conference papers
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, February 10, 2017 - 11:46:39 AM
Last modification on : Saturday, June 25, 2022 - 9:10:34 PM
Long-term archiving on: : Thursday, May 11, 2017 - 1:00:19 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Mounir Assaf, Julien Signoles, Frédéric Tronel, Eric Totel. Program Transformation for Non-interference Verification on Programs with Pointers. 28th Security and Privacy Protection in Information Processing Systems (SEC), Jul 2013, Auckland, New Zealand. pp.231-244, ⟨10.1007/978-3-642-39218-4_18⟩. ⟨hal-00814671v2⟩



Record views


Files downloads