%0 Conference Proceedings
%T Program Transformation for Non-interference Verification on Programs with Pointers
%+ Laboratoire Sûreté des Logiciels (LSL)
%+ Confidentialité, Intégrité, Disponibilité et Répartition (CIDRE)
%A Assaf, Mounir
%A Signoles, Julien
%A Tronel, Frédéric
%A Totel, Eric
%Z Part 4: Software Security
%< avec comité de lecture
%( IFIP Advances in Information and Communication Technology
%B 28th Security and Privacy Protection in Information Processing Systems (SEC)
%C Auckland, New Zealand
%Y Lech J. Janczewski
%Y Henry B. Wolfe
%Y Sujeet Shenoi
%I Springer Berlin Heidelberg
%3 Security and Privacy Protection in Information Processing Systems
%V AICT-405
%P 231-244
%8 2013-07-08
%D 2013
%R 10.1007/978-3-642-39218-4_18
%Z Cognitive science/Computer scienceConference papers
%X 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.
%G English
%Z TC 11
%2 https://inria.hal.science/hal-00814671v2/document
%2 https://inria.hal.science/hal-00814671v2/file/978-3-642-39218-4_18_Chapter.pdf
%L hal-00814671
%U https://inria.hal.science/hal-00814671
%~ CEA
%~ SUPELEC
%~ INSTITUT-TELECOM
%~ EC-PARIS
%~ UNIV-RENNES1
%~ CNRS
%~ INRIA
%~ UNIV-UBS
%~ INSA-RENNES
%~ INRIA-RENNES
%~ IRISA
%~ IRISA_SET
%~ INRIA_TEST
%~ SUP_CIDRE
%~ TESTALAIN1
%~ IFIP
%~ IFIP-AICT
%~ IRISA-D1
%~ DRT
%~ INRIA2
%~ IFIP-TC
%~ IFIP-TC11
%~ UR1-HAL
%~ IFIP-SEC
%~ UR1-MATH-STIC
%~ UR1-UFR-ISTIC
%~ IFIP-AICT-405
%~ TEST-UNIV-RENNES
%~ LIST
%~ TEST-UR-CSS
%~ UNIV-RENNES
%~ INRIA-RENGRE
%~ INSTITUTS-TELECOM
%~ UR1-MATH-NUM
%~ GS-SPORT-HUMAN-MOVEMENT