1 of 15

You Li*^a, Kaiyu Hou*^b, Yunqi He^a, Yan Chen^a, and Hai Zhou^a

^aNorthwestern University�^bAlibaba Cloud**

Property Guided Secure Configuration Space Search

ISC 2024, Arlington, VA

*Equal Contribution

**Any opinions, recommendations, or findings are those of the authors and do not reflect the

views of Alibaba Cloud.

[Title Slide] "Good afternoon everyone. I'm Yunqi He from Northwestern University. Today, I'm delighted to present our work on 'Property Guided Secure Configuration Space Search,' a collaborative effort with my colleagues You Li, Kaiyu Hou, advised by Professor Yan Chen, and Professor Hai Zhou.

Imagine you're a network system engineer tasked with configuring a complex reactive system. Not every configuration combination is risk-free - some might lead to security vulnerabilities or availability issues. Traditionally, you'd need to verify each configuration through time-consuming model checking. But in real-world deployments, we need something faster.

That's exactly what we'll be discussing today - how to enable real-time verification of system configurations while ensuring security and correctness.

[Moving to Outline] Let me outline what we'll cover in this presentation..."

2 of 15

Outline

2

Motivations and problem definition

The importance of configuration verification and drawbacks in current methods
Leverage “secure configuration space” to enable real-time verification

Technical contributions

Convert configuration verification into a model checking problem
Reduce the decision problem into a search problem
Heuristics to improve search coverage

Evaluations on testbenches and network protocols

[Outline Slide] "Here's what we'll cover today. First, I'll discuss our motivations and define the problem we're addressing. We'll explore why configuration verification is crucial and examine the limitations of current methods.

A key contribution of our work is the concept of 'secure configuration space' - which enables real-time verification. We'll see how this fundamental shift in approach makes a difference.

Then, I'll delve into our technical contributions. We'll explore how we:

Convert configuration verification into a model checking problem
(how we) Reduce the decision problem into a search problem
(and how we) Apply heuristics to improve search coverage

Finally, I'll share our evaluation results on various testbenches and network protocols, demonstrating the practical impact of our approach.

[Moving to Motivation] Let me start by explaining why configuration verification is so critical in today's networks..."

3 of 15

Motivation: Configuration Verification

3

Network configurations are constantly changing to:

support new services, accommodate new devices, enhance network security, etc.

Errors in configuration changes can cause catastrophic network outages:

56% of network incidents due to configuration changes in a leading cloud provider

Network configuration verification checks before deployment whether a new configuration satisfies a set of desired correctness properties:

reachability, way-pointing, loop-freedom…

[Motivation: Configuration Verification Slide]

"Networks are constantly evolving - we need to support new services, accommodate new devices, and enhance security measures. This means configurations are changing all the time.

But here's the critical issue: configuration changes can lead to catastrophic network outages. In fact, our research found that in a leading cloud provider, 56% of network incidents were directly attributed to configuration changes. This is a staggering number that highlights the importance of getting configurations right.

This is where network configuration verification comes in. It's a pre-deployment check to ensure that any new configuration satisfies a set of desired correctness properties. These properties include fundamental aspects like:

Reachability: Can all necessary endpoints communicate?
Way-pointing: Does traffic flow through required middleboxes?
Loop-freedom: Are there any routing loops?

[Moving to Drawbacks slide] However, current verification methods face significant challenges..."

4 of 15

Drawbacks of Existing Methods

4

Network verification is time consuming:

Verification out of time (24h) for Purdue topology (2159 nodes & 3,607 links)

Real-time network verification should be agile:

Check the correctness of configurations as they are deployed to real networks.

[Drawbacks of Existing Methods Slide]

"Let me highlight why current verification methods are not meeting today's needs. A major challenge is time. Network verification is incredibly time-consuming. Let me give you a concrete example: when testing the Purdue topology, which has 2,159 nodes and 3,607 links, the verification process couldn't complete even after 24 hours.

This brings us to a critical requirement: real-time network verification needs to be agile. Why? Because configurations are being deployed to real networks constantly. We can't afford to wait hours or days to verify each change.

Think about it: if your team needs to make an urgent security update to your network configuration, waiting 24 hours for verification isn't just impractical - it could be dangerous.

[Moving to Secure Configuration Space slide] This is where our key innovation comes in - the concept of secure configuration space..."

5 of 15

Secure Configuration Space

5

We aim to find a secure configuration space: any configurations within the space are guaranteed to be secure.
It reduces the original online decision problem into i) an offline search problem and ii) an online SAT query.
Additionally, it can suggest a correct alternative configuration that is as close as possible to the previous insecure configuration.

6 of 15

Secure Configuration Space

6

We aim to find a secure configuration space: any configurations within the space are guaranteed to be secure.

7 of 15

Advantages of Secure Configuration Space

7

It reduces the original online decision problem into i) an offline search problem and ii) an online SAT query.
Additionally, it can suggest a correct alternative configuration that is as close as possible to the previous insecure configuration.

[Advantages of Secure Configuration Space Slide]

"Let me elaborate on why this concept of secure configuration space is so powerful. It fundamentally changes how we approach configuration verification in two significant ways.

First, it transforms the problem from an online decision problem into two distinct parts:

The first one is An offline search problem, where we pre-compute the secure space. Yes, this part is computationally intensive, but it only needs to be done once.
And the second is A simple online SAT query, which can be executed in real-time. This means when a network engineer needs to verify a new configuration, they get an immediate answer.

Think about the practical implications: Instead of running a full model checking process every time you want to change a configuration, you just need to check if your proposed configuration falls within the pre-computed secure space. It's like having a map of all safe configurations at your fingertips.

But there's another powerful advantage that's particularly valuable in practice. When an engineer proposes a configuration that turns out to be insecure, our approach doesn't just say 'no' - it can actually suggest an alternative. And not just any alternative - it finds the closest secure configuration to what was proposed. This means:

Minimal disruption to existing setups
Faster problem resolution
More practical implementation of security measures

[Moving to Technical Contribution: Framework Slide] Now, let me show you how we actually achieve these benefits through our technical framework..."

8 of 15

Technical Contribution: Framework

8

9 of 15

Encode Configuration into State Space

9

We add configuration state variables alongside the normal state variables to implicitly encode configurations:

The configuration state variables are unconstrained at initialization, and their values remain unchanged during the execution.
In contrast, the normal state variables are constrained to the reset state at initialization, and their values can evolve as usual during the execution.

10 of 15

Enlargement of Secure Configuration Space

10

Inclusive Expansion: Suppose IV1 is the initial secure state space, we set IV1 as the initiation constraint and expands the secure state space to IV2
Parallel Expansion: we set S6 as the initiation constraint and start another search, thus yields a larger secure state space IV2 ∪ IV3

11 of 15

Enlargement of Secure Configuration Space

11

Inclusive Expansion: Suppose IV1 is the initial secure state space, we set IV1 as the initiation constraint and expands the secure state space to IV2

12 of 15

Enlargement of Secure Configuration Space

12

Parallel Expansion: we set S6 as the initiation constraint and start another search, thus yields a larger secure state space IV2 ∪ IV3

13 of 15

Evaluation: Safety Properties

13

(a) Safe benchmarks: our algorithm (INCISE) achieves better coverage, e.g., larger safe configuration space than others on safe benchmarks.

(b) Unsafe benchmarks: INCISE still works on unsafe benchmarks, while the other algorithms cannot find a valid invariant.

[Evaluation: Safety Properties Slide]

"We tested INCISE against both safe and unsafe benchmarks, and the results are quite striking.

Looking at graph (a), for safe benchmarks, INCISE achieves substantially better coverage than existing algorithms. In fact, we achieve 100% coverage in more than 50% of the benchmarks - that's a 55.7% improvement over other approaches.

Even more interesting is graph (b), showing results for unsafe benchmarks. While other algorithms simply fail to find valid invariants for unsafe benchmarks, INCISE continues to work effectively.

The result found by INCISE is agnostic to the initial configuration selected by the system engineer. This independence from initial conditions is crucial because it enables several practical applications, such as revision, iterative improvement, etc., which can guide the system engineer to find a secure and suitable configuration.

[Moving to Case Study: Cellular Emergency Protocols Slide]

But theoretical results are not enough - we needed to prove this works in real-world scenarios. Let me share a particularly important case study involving cellular emergency protocols.

14 of 15

Case Study: Cellular Emergency Protocols

14

[Case Study: Cellular Emergency Protocols Slide]

"Let me detail our cellular emergency protocols case study. Emergency call systems involve multiple participants with divergent requirements:

Different carriers have different concerns in configuring their systems
Each country has its own emergency numbers and regulations
The protocols keep evolving with major upgrades every decade and minor revisions quarterly

In our collaboration with three world-leading carriers and network device manufacturers, we realized it's impractical to provide a single universal configuration. We analyzed their emergency call system configurations and found a complex situation: while their configurations differed in many ways, all had violations of basic protocol requirements.

Let me share a concrete example of how challenging these issues can be. One carrier discovered that some emergency calls from their subscribers couldn't be properly routed. They attempted to fix this by modifying system configurations. However, our model checking revealed that their modification introduced another critical issue: roaming users couldn't dial emergency numbers when their screen was locked. This demonstrates why a trial-and-error approach to configuration isn't sufficient.

What makes INCISE particularly powerful here is its efficiency. The analysis completed in just milliseconds, achieving:

70.8% coverage with basic INCISE
100% coverage after applying expansion techniques

More importantly, our "minimum revision" approach helped these carriers fix all identified vulnerabilities while minimizing changes to their deployed systems. By providing a secure configuration space rather than a single fixed solution, we enabled carriers to find secure configurations that met their specific needs and constraints.

15 of 15

You Li*^a, Kaiyu Hou*^b, Yunqi He^a, Yan Chen^a, and Hai Zhou^a

^aNorthwestern University�^bAlibaba Cloud**

Thank you!