TY - GEN
T1 - Information flow monitoring as abstract interpretation for relational logic
AU - Chudnov, Andrey
AU - Kuan, George
AU - Naumann, David A.
N1 - Publisher Copyright:
© 2014 IEEE.
PY - 2014/11/13
Y1 - 2014/11/13
N2 - A number of systems have been developed for dynamic information flow control (IFC). In such systems, the security policy is expressed by labeling input and output channels, it is enforced by tracking and checking labels on data. Systems have been proven to enforce some form of noninterference (NI), formalized as a property of two runs of the program. In practice, NI is too strong and it is desirable to enforce some relaxation of NI that allows downgrading under constraints that have been classified as 'what', 'where', 'who', or 'when' policies. To encompass a broad range of policies, relational logic has been proposed as a means to specify and statically enforce policy. This paper shows how relational logic policies can be dynamically checked. To do so, we provide a new account of monitoring, in which the monitor state is viewed as an abstract interpretation of sets of pairs of program runs.
AB - A number of systems have been developed for dynamic information flow control (IFC). In such systems, the security policy is expressed by labeling input and output channels, it is enforced by tracking and checking labels on data. Systems have been proven to enforce some form of noninterference (NI), formalized as a property of two runs of the program. In practice, NI is too strong and it is desirable to enforce some relaxation of NI that allows downgrading under constraints that have been classified as 'what', 'where', 'who', or 'when' policies. To encompass a broad range of policies, relational logic has been proposed as a means to specify and statically enforce policy. This paper shows how relational logic policies can be dynamically checked. To do so, we provide a new account of monitoring, in which the monitor state is viewed as an abstract interpretation of sets of pairs of program runs.
KW - Abstract interpretation
KW - Declassification
KW - Endorsement
KW - Information flow
KW - Relational logic
KW - Run-time monitoring
UR - http://www.scopus.com/inward/record.url?scp=84939646275&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84939646275&partnerID=8YFLogxK
U2 - 10.1109/CSF.2014.12
DO - 10.1109/CSF.2014.12
M3 - Conference contribution
AN - SCOPUS:84939646275
T3 - Proceedings of the Computer Security Foundations Workshop
SP - 48
EP - 62
BT - Proceedings - 2014 IEEE 27th Computer Security Foundations Symposium, CSF 2014
T2 - 27th IEEE Computer Security Foundations Symposium, CSF 2014
Y2 - 19 July 2014 through 22 July 2014
ER -