자료유형  

 학위논문

Control Number  

0016935017

International Standard Book Number  

9798380414173

Dewey Decimal Classification Number  

004

Main Entry-Personal Name  

Wang, Qinshi.

Publication, Distribution, etc. (Imprint  

[S.l.] : Princeton University., 2023

Publication, Distribution, etc. (Imprint  

Ann Arbor : ProQuest Dissertations & Theses, 2023

Physical Description  

1 online resource(150 p.)

General Note  

Source: Dissertations Abstracts International, Volume: 85-03, Section: B.

General Note  

Advisor: Appel, Andrew W.

Dissertation Note  

Thesis (Ph.D.)--Princeton University, 2023.

Restrictions on Access Note  

This item must not be sold to any third party vendors.

Summary, Etc.  

요약P4 is a major standardized programming language for programming and specifying the network data plane. P4 is widely used in a variety of network functionalities, including monitoring, traffic management, forwarding, and security. Recently, stateful applications have been emerging in this area, as supported by programmable hardware. Typical stateful applications include network telemetry (heavy hitters, distributed denial-of-service (DDoS) detection, performance monitoring), middleboxes (firewalls, network address translation (NAT), load balancers, intrusion detection), and distributed services (in-network caching, lock management, conflict detection). Their complexity and rich properties are beyond the ability of existing P4 verifiers.In this thesis, we propose Verifiable P4: a new framework for P4 program verification based on interactive theorem proving that is (1) capable of proving multi-packet properties, (2) modular in terms of the structure of P4 programs, and (3) foundationally sound with respect to a mechanized formal semantics of P4. In order to achieve these goals, we built (1) a mechanized formal semantics of P4 more comprehensive and convenient than existing formal semantics, (2) a set of program logic rules that are proven sound, and (3) an interactive verification system based on the program logic and Coq tactic mechanism. We verified a stateful firewall fully implemented in P4 using a sliding-window Bloom filter with Verifiable P4 and evaluated its utility.

Subject Added Entry-Topical Term  

Computer science.

Subject Added Entry-Topical Term  

Computer engineering.

Subject Added Entry-Topical Term  

Logic.

Index Term-Uncontrolled  

Formal verification

Index Term-Uncontrolled  

Software-defined networking

Index Term-Uncontrolled  

Lock management

Added Entry-Corporate Name  

Princeton University Computer Science

Host Item Entry  

Dissertations Abstracts International. 85-03B.

Host Item Entry  

Dissertation Abstract International

Electronic Location and Access  

로그인을 한후 보실 수 있는 자료입니다.

Control Number  

joongbu:643426