Verifying Security Policies using Host Attributes

TL;DR

This paper introduces a method for verifying network security policies by expressing security invariants through host attributes, enabling automated configuration and verified in a civil aviation context.

Contribution

It presents a universal approach to formalize and verify security invariants for access control and information flow, with machine-verified proofs using Isabelle/HOL.

Findings

Universal insights about security invariants

Automated host attribute configuration

Verification demonstrated in civil aviation scenario

Abstract

For the formal verification of a network security policy, it is crucial to express the verification goals. These formal goals, called security invariants, should be easy to express for the end user. Focusing on access control and information flow security strategies, this work discovers and proves universal insights about security invariants. This enables secure and convenient auto-completion of host attribute configurations. We demonstrate our results in a civil aviation scenario. All results are machine-verified with the Isabelle/HOL theorem prover.