SDN & Cloud
Network Optimizing for Microservices / Serverless Cloud (work in progress)
2020 – Present

Microservices/serverless architectures bring flexibility but introduce network communication delay.

The connection setup latency is no longer negligible for auto-scaled ephemeral workers, as we cannot simply mitigate it by using persistent connections.

We seamlessly integrate QUIC into OpenFaaS/Kubernetes to improve network performance, without any user code change.

Systematic benchmarks are also designed for the microservices/serverless network performance measurement.

Generic Security Policy Enforcement System for SDN-based Cloud
2017 – 2018

We design a policy language for resource protection and management of SDN-based Cloud.

The policy enforcement system is implemented in the OpenDaylight controller, and deployed on OpenStack.

Routing Policy for Solving Reactive Model Overhead of SDN
2016 – 2017

SDN control channel bandwidth is the major bottleneck of applying reactive forwarding.

By leveraging the SDN fine-grained flow control ability, we proposed a routing policy to reduce the control channel bandwidth consumption up to 80%.

This policy is implemented in the Floodlight controller under OpenFlow, and deployed on Open vSwitch and ONetSwitch (an OpenFlow/P4 white-box switch).

Formal Methods for Network Protocols
Formal Secure Configuration Search for Network Protocols
2020 – 2021

Traditionally, researchers use secure properties to verify a protocol is safe or find counterexamples.

We convert this decision problem into a search problem. Given the model and the properties, we search the boundaries of the configuration space where the system is always secure and reliable.

We employ inductive generalization and improved IC3 algorithm to determine the space.

Formal Verification and Vulnerability Detection of LTE/5G Protocols
2019 – 2020

This project aims to formally detect vulnerabilities in 3GPP protocols.

The 4G/5G emergency call protocols and systems are formally specified in TLA+, and then checked by model checker.

A complete cellular network testbed from RAN, edge to core (USRP, OpenAirInterface) is built for cross-verification.

Serious real-world availability and security pitfalls are discovered, and acknowledged by major cellular carriers.