GrammaTech ConfINE

GrammaTech ConfINE is a framework that enables systematic and rigorous modeling of access control in complex, network-composed systems. It uses logic to capture and reason about global access control properties, determining which categories of system users are capable of accessing various system resources. The framework formally links together the capabilities and configuration of individual components to enable uniform and systematic querying of system-wide access-control properties. The resulting model captures system architecture (network topology, firewall and routing configurations), device setup (user configuration, file permissions, public-key infrastructure), services (remote access, web access configurations), user knowledge (system-access credentials), and low-level vulnerabilities (CVEs and zero-days). ConfINE supports queries such as whether specific services are accessible from external networks, whether users with low-privilege accounts can access sensitive data, and what set of system users has access to specific resources. The framework provides capabilities for penetration testing and red teaming, internal threat minimization, forensic analysis, symbolic configuration analysis, and automated configuration synthesis. It relies on an extensible library of model building blocks including network interfaces, firewall rules, Linux and Windows users and files, OpenSSH, Apache Web Server, and others. Models are expressed as sets of logical formulas (horn clauses) and can be queried mechanically using automated decision procedures such as prolog or datalog interpreters.