Enforcing Trace Properties by Program Transformation

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. 1 Motivation and approach Programming can be seen as the task of implementing a collection of properties (the specification). Let us focus on two problems the programmer may face in...

• Type: Conference
• Year: 2000
• Where: POPL
• Authors: Thomas Colcombet, Pascal Fradet
• Keywords: POPL 2000, Programming Languages, Static Analyses, Static Program Analyses, Trace Properties