Network Verification
With the increasing size and complexity of computer networks, it is difficult for network administrators to ensure that the network intent has been correctly implemented, and incorrect network configurations will affect the security and availability of the network. Inspired by the successful application of formal methods in the field of hard and software verification, researchers have applied formal methods to networking, resulting in a new research area, namely Network Verification, which aims to prove the correctness of networks using rigorous mathematical methods.
Our group works on 1) Accelerating the data plane and control plane verification. 2) Achieving privacy-preserving verification. 3) Diagnosing and repairing configuration errors with high efficiency and interpretability after verification.
Network Programming
The traditional network is a passive network, which passively receives the packets from the outside and processes the packets according to the existing protocol. The emergence of programmable networks makes the network active instead of passive, and some network applications can be offloaded to the network. Software-Defined Network (SDN) separates the control plane from the network node to the software platform, replacing the traditional embedded and inflexible control plane with an open software model. Programming Protocol-Independent Packet Processor (P4) transforms the data plane into a programmable network platform, greatly improving the flexibility and availability of the data plane.
Our group is currently taking advantage of the programmable network data plane to optimize some traditional applications: 1) Designing entirely new protocols to utilize the hardware resources of the data plane to accelerate certain algorithms; 2) optimizing distributed applications by taking advantage of the feature that data plane is on the way to the packet.
Interpretable Machine Learning
In recent years, machine learning has been widely used in computer vision, natural language processing, computer networking, etc., and has proved to have outstanding performance. However, due to the black-box nature of the machine learning system itself, we cannot fully understand the results of the model, which is not conducive to further improvement of model design and large-scale deployment of related systems.
Our group investigates how to provide more efficient interpretability for machine learning systems by (1) studying various verification problems, and interpretability problems, trying to formalize them into a uniform format; (2) implementing a general framework to automatically verify and explain the behavior of a wide range of machine learning systems faster and more accurately.
Congestion Control
The congestion control algorithm is an effective algorithm to improve network performance. Nowadays, the increase in network size, data volume, and more refined quality of service requirements make the network face more complex application scenarios. Traditional congestion control cannot cope well with these complex network scenarios, which leads to large performance losses.
Our group's research mainly includes (i) Providing appropriate congestion control algorithms for complex network scenarios and application abstractions, integrating into a unified congestion control mechanism. (ii) Improving the effectiveness of congestion control algorithms using NOVEL Network Devices to enhance the overall performance of the network.
