Enforcing trace properties by program transformation

Thomas Colcombet 1 Pascal Fradet 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We propose an automatic method to enforce trace properties on programs. The programmer specifies the property separately from the program; a program transformer takes the program and the property and automatically produces another ``equivalent'' program satisfying the property. This separation of concerns makes the program easier to develop and maintain. Our approach is both static and dynamic. It integrates static analyses in order to avoid useless transformations. On the other hand, it never rejects programs but adds dynamic checks when necessary. An important challenge is to make this dynamic enforcement as inexpensive as possible. The most obvious application domain is the enforcement of security policies. In particular, a potential use of the method is the securization of mobile code upon receipt.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00000937
Contributor : Pascal Fradet <>
Submitted on : Thursday, December 15, 2005 - 4:07:19 PM
Last modification on : Friday, November 16, 2018 - 1:23:42 AM
Long-term archiving on : Saturday, April 3, 2010 - 7:19:16 PM

Identifiers

  • HAL Id : inria-00000937, version 1

Citation

Thomas Colcombet, Pascal Fradet. Enforcing trace properties by program transformation. Principles of Programming Languages, Jan 2000, Boston. ⟨inria-00000937⟩

Share

Metrics

Record views

395

Files downloads

225