Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
422015 | Electronic Notes in Theoretical Computer Science | 2009 | 15 Pages |
Abstract
Many information-flow type systems have been developed that allow to control the non-interference of information between the levels of classification in the Bell-LaPadula model. We present here a translation of typing information collected for bytecode programs to a bytecode program logic. This translation uses the syntax of a bytecode specification language BML. A translation of this kind allows including the check of the non-interference property in a single, unified verification framework based on a program logic and thus can be exploited within a foundational proof-carrying code infrastructure. It also provides a flexible basis for various declassification strategies that may be useful in a particular code body.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics