### Abstract

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.

- Secure auto-completion of scenario-specific knowledge, which eases usability.
- Security violations can be repaired by tightening the policy iff the security invariants hold for the deny-all policy.
- An algorithm to compute a security policy.
- A formalization of stateful connection semantics in network security mechanisms.
- An algorithm to compute a secure stateful implementation of a policy.
- An executable implementation of all the theory.
- Examples, ranging from an aircraft cabin data network to the analysis of a large real-world firewall.
- More examples: A fully automated translation of high-level security goals to both firewall and SDN configurations (see Examples/Distributed_WebApp.thy).

For a detailed description, see

- C. Diekmann, A. Korsten, and G. Carle. Demonstrating topoS: Theorem-prover-based synthesis of secure network configurations. In 2nd International Workshop on Management of SDN and NFV Systems, manSDN/NFV, Barcelona, Spain, November 2015.
- 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.
- 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.

### License

BSD License

### History

April 14, 2015
  Added Distributed WebApp example and improved graphviz visualization (revision 4dde08ca2ab8)

### Topics

- Computer science/Security

### Session Network_Security_Policy_Verification

- ML_GraphViz
- ML_GraphViz_Disable
- FiniteGraph
- FiniteListGraph
- TopoS_Util
- Efficient_Distinct
- FiniteListGraph_Impl
- TopoS_Vertices
- TopoS_Interface
- TopoS_withOffendingFlows
- TopoS_ENF
- vertex_example_simps
- TopoS_Helper
- SINVAR_Subnets2
- SINVAR_BLPstrict
- SINVAR_Tainting
- SINVAR_BLPbasic
- SINVAR_TaintingTrusted
- SINVAR_BLPtrusted
- Analysis_Tainting
- TopoS_Interface_impl
- SINVAR_BLPbasic_impl
- SINVAR_Subnets
- SINVAR_Subnets_impl
- SINVAR_DomainHierarchyNG
- SINVAR_DomainHierarchyNG_impl
- SINVAR_BLPtrusted_impl
- SINVAR_SecGwExt
- SINVAR_SecGwExt_impl
- SINVAR_Sink
- SINVAR_Sink_impl
- SINVAR_SubnetsInGW
- SINVAR_SubnetsInGW_impl
- SINVAR_CommunicationPartners
- SINVAR_CommunicationPartners_impl
- SINVAR_NoRefl
- SINVAR_NoRefl_impl
- SINVAR_Tainting_impl
- SINVAR_TaintingTrusted_impl
- SINVAR_Dependability
- SINVAR_Dependability_impl
- SINVAR_NonInterference
- SINVAR_NonInterference_impl
- SINVAR_ACLcommunicateWith
- SINVAR_ACLnotCommunicateWith
- SINVAR_ACLnotCommunicateWith_impl
- SINVAR_ACLcommunicateWith_impl
- SINVAR_Dependability_norefl
- SINVAR_Dependability_norefl_impl
- TopoS_Library
- TopoS_Composition_Theory
- TopoS_Stateful_Policy
- TopoS_Composition_Theory_impl
- TopoS_Stateful_Policy_Algorithm
- TopoS_Stateful_Policy_impl
- METASINVAR_SystemBoundary
- TopoS_Impl
- Network_Security_Policy_Verification
- Example_BLP
- TopoS_generateCode
- attic
- Impl_List_Playground_ChairNetwork
- Impl_List_Playground_statefulpolicycompliance
- Example
- Example_NetModel
- Example_Forte14
- Distributed_WebApp
- I8_SSH_Landscape
- Impl_List_Playground
- Impl_List_Playground_ChairNetwork_statefulpolicy_example
- CryptoDB
- IDEM
- MeasrDroid
- SINVAR_Examples
- Imaginary_Factory_Network

### Depends on

- Automatic Data Refinement
- Executable Transitive Closures of Finite Relations

## Cite

×

Network_Security_Policy_Verification-AFP

    @article{Network_Security_Policy_Verification-AFP,
      author  = {Cornelius Diekmann},
      title   = {Network Security Policy Verification},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Network_Security_Policy_Verification.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Jul 9, 2014 : Isabelle2013-2