Email Gateway (Aug 19 2022 at 15:15): Email Gateway (Aug 19 2022 at 15:15):From: Tobias Nipkow <nipkow@in.tum.de>
Network Security Policy Verification
Cornelius Diekmann
http://afp.sourceforge.net/entries/Network_Security_Policy_Verification.shtml
We present a unified theory for verifying network security policies. A security
policy is represented as directed graph. To check high-level security goals,
security invariants over the policy are expressed. We cover monotonic security
invariants, i.e. prohibiting more does not harm security. We provide the
following contributions for the security invariant theory.
(i) Secure auto-completion of scenario-specific knowledge, which eases usability.
(ii) Security violations can be repaired by tightening the policy iff the
security invariants hold for the deny-all policy.
(iii) An algorithm to compute a security policy.
(iv) A formalization of stateful connection semantics in network security
mechanisms.
(v) An algorithm to compute a secure stateful implementation of a policy.
(vi) An executable implementation of all the theory.
(vii) Examples, ranging from an aircraft cabin data network to the analysis of a
large real-world firewall.
For a detailed description, see
C. Diekmann, S.-A. Posselt, H. Niedermayer, H. Kinkelin, O. Hanka, and G. Carle.
Verifying Security Policies using Host Attributes.
In FORTE – 34th IFIP International Conference on Formal Techniques for
Distributed Objects, Components and Systems, Berlin, Germany, June 2014.
http://www.net.in.tum.de/pub/diekmann/forte14.pdf
C. Diekmann, L. Hupel, and G. Carle. Directed Security Policies: A Stateful
Network Implementation.
In J. Pang and Y. Liu, editors, Engineering Safety and Security Systems, volume
150 of Electronic Proceedings in Theoretical Computer Science, pages 20–34,
Singapore, May 2014. Open Publishing Association.
http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?ESSS2014.3
Enjoy!
Last updated: Nov 21 2024 at 12:39 UTC