ConfINE

Cyber security has utmost importance across the entire spectrum of computer applications, from personal use to commercial to national critical infrastructure. Over the last few decades, a number of techniques for systematic modeling and security analysis of computer systems have been developed (including an extensive portfolio of GrammaTech technology). This technology focuses on and excels at detecting individual vulnerabilities in stand-alone software modules. The overarching goal of cyber security, however, is to prevent illicit or unauthorized access to the system and the data it manipulates: 

  • Prevent attackers from corrupting or stealing sensitive data, 
  • Prevent attackers from gaining control over or compromising a device, 
  • Prevent attackers from hiding their presence and covering their tracks. 

In this larger context, individual vulnerabilities and their exploits are just “a means to an end” for the attacker. A typical real-world attack consists of many steps that may include social engineering (e.g., tricking users into revealing their passwords), misconfiguration abuse (e.g., overly lax firewall rules), regular system operations (e.g., exploring the system under an assumed identity), in addition to actual vulnerability exploits. Constructing successful attacks is a non-trivial undertaking – it may take a red-team months of manual exploration and planning to execute an attack. Countering attack is not easy either – it requires constant vigilance from IT staff to maintain system security without compromising its mission. 

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. ConfINE provides capabilities for: 

  • Ensuring that legal system users can access the resources they need to accomplish their tasks and vice versa (preventing them from accessing resources that are not required). 
  • Constructing attack graphs for realizing illicit access to system resources, capturing sequences of vulnerability exploits mixed in with regular system operations. 
  • Gauging the severity of the system’s latent vulnerabilities to triage and expedite attack mitigation.  

Modern software systems are built by composing many independent components – operating systems, webservers, application servers, containerization and virtualization platforms, mission-specific logic, etc.  Many of these components are deliberately designed to be versatile so that they can be effectively used in many different contexts. When a system is constructed, the components are configured and interfaced with each other to enable end-to-end system operation. The global system-wide access control is achieved by combining and configuring facilities provided by individual components. This is an intricate system-specific effort that is largely performed manually, and thus, is time-consuming and error-prone.  

ConfINE 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, etc. 
  • Device setup: user configuration, file permissions, public-key infrastructure, etc. 
  • Services: remote access (e.g., ssh, ftp configuration), web access (e.g., apache, nginx configuration), etc. 
  • User knowledge: e.g., system-access credentials 
  • Low-level vulnerabilities: extant CVEs and detected zero-days contained by the software the system runs. 


Sample queries that ConfINE supports include: 

  • Is a specific service (e.g., company intranet) accessible from an external network? 
  • Can a user with remote access to a low-privilege (e.g., intern) account get access to sensitive company data stored on a secure server? 
  • What set of system users has access to a specific resource (e.g., HR’s employee database)? 

ConfINE provides a formal foundation enabling several important cyber-security applications: 

  • Penetration Testing and Red Teaming. Can an outsider with minimal knowledge gain access to the system’s sensitive data? If so, how? What is the sequence of operations to execute?  
  • Internal Threat Minimization. Find system users with privileges that are not required for system functionality. Support mechanisms for ensuring that access privileges are properly revoked. 
  • Forensic Analysis. Establish the breach perimeter after the system has been breached: identify data that can still be trusted. 
  • Symbolic Configuration Analysis. Check non-trivial security and functionality properties. Assess how local configuration changes affect system-wide behavior. 
  • Automated Configuration Synthesis: Support mechanisms that generate/augment system configuration in a way that enables system functionality while minimizing its attack surface.  

To model system behavior, ConfINE relies on an extensible library of model building blocks: e.g., network interfaces, firewall rules, Linux and Windows users and files, OpenSSH, Apache Web Server, and many others. These building blocks are used to automatically construct models of complex systems based on the collected system information. The models are expressed as sets of logical formulas (i.e., horn clauses) and can be queried mechanically using automated decision procedures (e.g., a prolog or datalog interpreter). 

The video below is a presentation of ConfINE, originally given at the HCSS 2022 conference.