×

Modelling declassification policies using abstract domain completeness. (English) Zbl 1252.68079

Summary: This paper explores a three dimensional characterisation of a declassification-based non-interference policy and its consequences. Two of the dimensions consist in specifying
(a) the power of the attacker, that is, what public information a program has that an attacker can observe; and
(b) what secret information a program has that needs to be protected.
Both these dimensions are regulated by the third dimension
(c) the choice of program semantics, for example, trace semantics or denotational semantics, or any semantics in Cousot’s semantics hierarchy.
To check whether a program satisfies a non-interference policy, one can compute an abstract domain that over-approximates the information released by the policy and then check whether program execution can release more information than permitted by the policy. Counterexamples to a policy can be generated by using a variant of the Paige-Tarjan algorithm for partition refinement. Given the counterexamples, the policy can be refined so that the least amount of confidential information required for making the program secure is declassified.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing

Software:

Octagon
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Askarov, Proceedings IEEE Symposium on Security and Privacy (2007)
[2] DOI: 10.1145/1255329.1255339 · doi:10.1145/1255329.1255339
[3] DOI: 10.1007/11787006_10 · Zbl 1133.94307 · doi:10.1007/11787006_10
[4] DOI: 10.1007/s10990-006-8609-1 · Zbl 1105.68069 · doi:10.1007/s10990-006-8609-1
[5] Mastroeni, Springer-Verlag Lecture Notes in Computer Science 4905 pp 147– (2008)
[6] DOI: 10.1007/11575467_27 · doi:10.1007/11575467_27
[7] Li, Proceedings of the 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’05) pp 158– (2005)
[8] DOI: 10.1007/BFb0039592 · doi:10.1007/BFb0039592
[9] DOI: 10.1016/S0167-6423(99)00024-6 · Zbl 0954.68052 · doi:10.1016/S0167-6423(99)00024-6
[10] DOI: 10.1007/11547662_13 · doi:10.1007/11547662_13
[11] Goguen, Proceedings IEEE Symposium on Security and Privacy pp 75– (1984)
[12] Winskel, The formal semantics of programming languages: an introduction (1993) · Zbl 0919.68082
[13] DOI: 10.1145/1134744.1134750 · doi:10.1145/1134744.1134750
[14] DOI: 10.1007/11924661_12 · Zbl 1168.68364 · doi:10.1007/11924661_12
[15] DOI: 10.1109/CSFW.2001.930133 · doi:10.1109/CSFW.2001.930133
[16] DOI: 10.1023/A:1011553200337 · Zbl 0967.68039 · doi:10.1023/A:1011553200337
[17] DOI: 10.1109/JSAC.2002.806121 · doi:10.1109/JSAC.2002.806121
[18] DOI: 10.1007/978-3-540-37621-7_9 · doi:10.1007/978-3-540-37621-7_9
[19] DOI: 10.1007/978-3-540-31980-1_10 · doi:10.1007/978-3-540-31980-1_10
[20] DOI: 10.1137/0216062 · Zbl 0654.68072 · doi:10.1137/0216062
[21] Myers, Proceedings IEEE Symposium on Security and Privacy pp 21– (2004)
[22] DOI: 10.1145/333979.333989 · Zbl 1133.68370 · doi:10.1145/333979.333989
[23] DOI: 10.1007/3-540-47764-0_20 · doi:10.1007/3-540-47764-0_20
[24] DOI: 10.1007/978-3-540-31987-0_21 · doi:10.1007/978-3-540-31987-0_21
[25] DOI: 10.1145/964001.964017 · Zbl 1325.68043 · doi:10.1145/964001.964017
[26] DOI: 10.1145/360933.360975 · Zbl 0308.68017 · doi:10.1145/360933.360975
[27] DOI: 10.1145/1067625.806556 · doi:10.1145/1067625.806556
[28] Di Pierro, Proceedings of the IEEE Computer Security Foundations Workshop pp 1– (2002)
[29] DOI: 10.1007/978-3-540-32004-3_20 · doi:10.1007/978-3-540-32004-3_20
[30] DOI: 10.1145/567752.567778 · doi:10.1145/567752.567778
[31] Banerjee, Proceedings IEEE Symposium on Security and Privacy (2008)
[32] DOI: 10.1145/512950.512973 · doi:10.1145/512950.512973
[33] Banerjee, Electronic Notes in Theoretical Computer Science 1514 (2007)
[34] DOI: 10.1016/S0304-3975(00)00313-3 · Zbl 0996.68119 · doi:10.1016/S0304-3975(00)00313-3
[35] Amtoft, Proceedings of the 33rd Annual ACM Symposium on Principles of Programming Languages pp 91– (2006)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.