Proof-Carrying Network Code - Department Of Computer Science
Proof-Carrying Network CodeChristian SkalkaJohn RingDavid DaraisUniversity of VermontBurlington, VT, USAceskalka@uvm.eduUniversity of VermontBurlington, VT, USAjohn.ring@uvm.eduUniversity of VermontBurlington, VT, USAddarais@uvm.eduMinseok KwonSahil GuptaKyle DillerRochester Institute of TechnologyRochester, NY, USAjmk@cs.rit.eduRochester Institute of TechnologyRochester, NY, USAsg5414@rit.eduRochester Institute of TechnologyRochester, NY, USAkid6584@rit.eduSteffen SmolkaNate FosterCornell UniversityIthaca, NY, USAsmolka@cs.cornell.eduCornell UniversityIthaca, NY, USAjnfoster@cs.cornell.eduABSTRACTComputer networks often serve as the first line of defense againstmalicious attacks. Although there are a growing number of toolsfor defining and enforcing security policies in software-definednetworks (SDNs), most assume a single point of control and areunable to handle the challenges that arise in networks with multipleadministrative domains. For example, consumers may want wantto allow their home IoT networks to be configured by device vendors, which raises security and privacy concerns. In this paper wepropose a framework called Proof-Carrying Network Code (PCNC)for specifying and enforcing security in SDNs with interacting administrative domains. Like Proof-Carrying Authorization (PCA),PCNC provides methods for managing authorization domains, andlike Proof-Carrying Code (PCC), PCNC provides methods for enforcing behavioral properties of network programs. We developtheoretical foundations for PCNC and evaluate it in simulated andreal network settings, including a case study that considers securityin IoT networks for home health monitoring.CCS CONCEPTS Security and privacy Formal methods and theory of security; Software and its engineering Formal softwareverification; Networks Programming interfaces; Network security;KEYWORDSTrust Management; Formal Verification; Software-Defined Networks; Nexus Authorization Logic; NetKATPermission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. Copyrights for components of this work owned by others than ACMmust be honored. Abstracting with credit is permitted. To copy otherwise, or republish,to post on servers or to redistribute to lists, requires prior specific permission and/or afee. Request permissions from permissions@acm.org.CCS ’19, November 11–15, 2019, London, United Kingdom 2019 Association for Computing Machinery.ACM ISBN 978-1-4503-6747-9/19/11. . . 15.00https://doi.org/10.1145/3319535.3363214ACM Reference Format:Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta,Kyle Diller, Steffen Smolka, and Nate Foster. 2019. Proof-Carrying NetworkCode. In 2019 ACM SIGSAC Conference on Computer and CommunicationsSecurity (CCS ’19), November 11–15, 2019, London, United Kingdom. ACM,New York, NY, USA, 15 pages. ONComputer networks play a critical role in implementing securitypolicies, often serving as the first line of defense against maliciousattacks. Although there are a growing number of tools for specifyingand verifying behavior in software-defined networks (SDNs), mostare unable to handle the challenges that arise in networks withmultiple administrative domains.To illustrate, consider the following concrete scenario. Supposethat a health monitoring system is connected to a home networkwith one or more IoT (Internet of Things) devices—e.g., as shownin Figure 1(a), a fitness tracker monitors the sleep patterns of itsresidents, using Bluetooth or WiFi to connect to a switch thatprovides connectivity to other devices on the local network. There isalso an edge router that connects the home network to the Internet.To prevent health data from being sent externally, the networkis configured as follows. The switch uses VLANs (virtual localarea networks) to isolate different segments of the network fromeach other, while the router uses a firewall to filter incoming andoutgoing traffic and a NAT (network address translator) to convertbetween private addresses used in the home network and publicaddresses used on the Internet. For example, the switch mightclassify packets coming from the fitness tracker, adding a tag toindicate if they are private (e.g., fine-grained location information)or public (e.g., aggregate, anonymous sleep data), and the firewallmight drop packets tagged as private.Suppose we add a second device that monitors blood pressure.In order to report information in an emergency—e.g., when bloodpressure becomes dangerously high—the network must be reconfigured. In particular, the filtering rules installed on the firewall mustbe relaxed to allow data to be released from the network even ifit is not public during an emergency. One possible approach is to
CCS ’19, November 11–15, 2019, London, United Kingdomedge routersleeptrackercloudserverpublicdataprivate data(a) Initially, only public data generated by the sleep tracker can pass theedge vate data(b) After the blood pressure monitor is added, the emergency data is notfiltered at the router reaching the 911 ivatedatapublicML server(c) Public data from the sleep tracker is delivered to a federated edgecomputing service upon request.Figure 1: PCNC use case: health monitoring edge network.modify the switch to apply a special emergency tag and relax thefiltering rules used by the firewall to forward packets carrying thistag, even if they are also marked as private.Although this is a simple example, it already raises a number ofinteresting issues. First, to correctly configure the network, we mustspecify, verify, and coordinate behavior on multiple devices—e.g.,the tagging rules at the switch and the filtering rules at the firewall.Second, we must ensure that requests to reconfigure devices aresubmitted by an authorized party. For example, the homeownermight only trust device vendors that have been appropriately certified. Unfortunately, existing platforms do not provide adequatemechanisms for specifying and enforcing such properties.Moreover, challenges related to security and federation arise inmore complex and varied systems, such as the following scenarios.Campus Network: The goal is to implement a distributed firewallthat isolates different classes of traffic from each other—e.g., faculty,students, and visitors. However, different principals are responsiblefor managing the devices in the network. For instance, universitystaff might control the routers at the core of the network whiledepartment staff control the switches at the edge.Internet Exchange Point (IXP): The goal is to allow each participant to specify policies that determine how their own traffic ishandled. These policies encode intricate preferences and are oftenSkalka et al.inter-dependent, due to complex business relationships and operational concerns—e.g., a large Internet Service Provider (ISP) mightbe willing to carry traffic generated by its direct customers, but notbe willing to provide transit for competitors.Federated Edge Computing: The goal is to push computationaltasks to edge devices, which requires using the network to communicate the inputs and outputs of a given computation. For example,the IoT network (B) described above might coordinate with anotherIoT network (A) that provides a machine learning (ML) service atthe edge, allowing A to configure B to forward public data to Aas illustrated in Figure 1(c). However, authorization is challengingin this context since A and B may not have a direct trust relationship, and A and B may have independent local policies governingauthorization and network behavior.In each scenario, multiple principals must collaborate to managedifferent network devices and enforce the intended security policy. However, operators often have no choice but to rely on socialmechanisms or even blind faith. This is unfortunate since networkscan provide crucial security and privacy defenses. For example,networks can prevent sensitive information from being exfiltratedby monitoring and blocking unauthorized communication. Theycan ensure that data received from untrusted sources is properlysanitized before it is sent to internal servers. And they can providestrong guarantees about availability, even in the presence of congestion or failures, by setting up multiple, redundant paths connectingeach pair of hosts.A promising approach to these problems is to exploit the programming interface for network devices provided by softwaredefined networks (SDN). However existing SDN platforms eitherassume a single administrative domain, or only handle limitedforms of federation—e.g., virtualization solutions that enable multiple tenants to control disjoint slices of the network. For instance,languages such as Frenetic [12], Pyretic [28], and NetKAT [4], anddata plane verification tools such as Header Space Analysis [22]and Veriflow [23] assume that the network is managed by a singleadministrator who has global visibility of the network and full authority to control how packets are processed. SDN control platformsalso present their own unique security challenges [25, 32].1.1Overview and FoundationsTo address these challenges, we introduce an expressive and flexiblediscipline for reconfiguring SDN controllers in a federated settingthat supports both authorization and behavioral compliance ofprograms, called Proof-Carrying Network Code (PCNC). Analogousto Proof-Carrying Code (PCC) [29], PCNC allows clients to shipproofs of security compliance along with their code that can beverified before it is installed. We argue that networks are a goodapplication domain for a PCC-style approach for several reasons.First, as discussed above, operators today must often execute programs produced by different parties with varying degrees of trust.Hence, a framework in which rich properties are automaticallyverified using a trustworthy proof checker could have a significantpractical impact. Second, while networks are often large in size,the programs they execute tend to be extremely simple and thusamenable to verification—each device executes a loop-free programthat classifies and transforms incoming packets.
Proof-Carrying Network CodeWe observe that there are two key concerns for allowing networkreconfiguration across multiple administrative domains: authorizing that a network update is permitted, and verifying that the updatepreserves important behavioral properties. To this end, PCNC usesa client-server model in which administrators can submit policyspecifications of authorization and behavior and clients can submitauthorization credentials and network updates. Upon receiving aclient request, the server verifies it against its current authorizationand behavioral policies.PCNC is based on two existing theories, which provide its formalfoundation: Nexus Authorization Logic (NAL) [19, 35] for expressing and enforcing authorization policies, and NetKAT for expressingand enforcing behavioral policies. NetKAT is a domain-specific language for programming and reasoning about SDNs developed inprevious work [4, 13]. It is based on a solid mathematical foundation, Kleene Algebra with Tests (KAT) [24], and comes equippedwith an equational reasoning system that can be used to verifymany properties of interest automatically [13].1.2Contributions and Related WorkIn this paper we develop theory and establish an architecture forPCNC, including a prototype implementation and evaluation onrealistic use cases both in simulation and on a hardware testbed.In Section 2, we describe the theoretical foundations of PCNC.We formulate a variant of NAL, called NALlight , that capturesapplication-level assertions about NetKAT programs. Thus, judgments in NALlight model an authorization and a behavioral component. The authorization component combines the expressiveness ofa higher-order logic extended with modalities for belief ascriptionand delegation, while properties involving NetKAT programs canbe expressed as application-level assertions (though decidable properties, such as equivalence, are of particular interest). For propertiesthat can be reduced to equivalence, we define an algorithm withoptimizations for checking equivalence of NetKAT programs thatis based on previous work [13].Also in Section 2, we develop a language for proof representation,called System FSays , a typed term calculus that enjoys a CurryHoward types-as-formulas correspondence with NALlight as statedin Theorem 2.1. Our approach to proof representation is similar toCDD [2], which demonstrated the benefits of the Curry-Howardapproach, including a reduction semantics that can support proofminimization.In Section 3, we describe how these elements are combined ina system for enforcing security in SDNs. We propose a specificjudgment form that can be used to verify requests to either reconfigure or extend the configuration of the network using NetKAT.Verification of requests subsumes System FSays type checking forauthorization and decidable equivalence checking for behavioralverification. Classic work on PCC focuses mostly on supportingpurely behavioral policies, but previous work has considered ProofCarrying Authentication [5] and Authorization [6, 15], also knownas PCA, to support verification of authorization policies in distributed systems. Thus, PCNC unifies concepts explored in PCCand PCA to obtain a uniform language framework for expressingproofs of authorization and behavioral policy compliance to supportSDN network configuration in federated settings.CCS ’19, November 11–15, 2019, London, United KingdomThe work most related to our PCNC framework is the FLANCsystem [18]. However, being based on NAL and NetKAT, PCNCoffers effective mechanisms for constructing proofs and decidingbehavioral properties that are based on well-studied logical foundations. In particular, since PCNC requests carry System FSays proofwitnesses, authorization is based on proof checking, not proof reconstruction or certificate chain discovery, unlike systems such asSAFE [7].In Section 4, we develop a case study that illustrates its featuresand applicability to SDN programming. This case study is basedon the IoT health monitoring network example discussed aboveand illustrated in Figure 1. We propose a specific network topology,configurations, and PCNC requests that embody the example.In Section 5. we describe an implementation of PCNC on a hardware testbed that combines novel verification components withNetKAT compilation tools from Frenetic [12], as described in Section 5.2. Our implementation includes a JSON wire format schemafor PCNC messages and and a signature verification scheme forNALlight credentials. We evaluate the implementation using thecase study and report on verification overhead.2PCNC FOUNDATIONSIn this section we develop a foundational theory for PCNC. Tosupport authorization in PCNC, we adapt the authorization logicNAL [35]. We define a natural deduction style proof theory forthe logic, for which we later develop a proof representation andchecking method in Section 2.1.4.To support behavioral policy specification and enforcement during network reconfiguration, we use the NetKAT language [4, 13].NetKAT has a decidable equational theory—here, we define an algorithm for checking program equivalence that is incorporated intoour PCNC framework to support behavioral verification.2.1Authorization LogicA number of authorization logics have been proposed in previouswork that offer features for policy expression [1, 3, 8, 17, 19]. In general, modern authorization logics equate authorization decisionswith provability of formulas, where given authorization credentials are modeled as assumptions for the proof derivation. Theytypically extend an underlying logic (e.g., first-order classical logic)with SpeaksFor and Says modalities endowed with either a possible worlds semantics [16] or a related semantics of “belief” [19].The SpeaksFor modality allows the authority of one principal to be“handed off” to another, supporting expression of the delegation ofauthority. The Says modality is typically taken to ascribe beliefs toprincipals and can be used to express authorized credentials amongothers, but the precise interpretation of Says is a subtle matter withsignificant consequences. We discuss this issue here as it is relevantto our proof representations.2.1.1 Monadic Interpretation of Says. The Says modality hashistorically been related to classical modalities. The interpretationof Says in the original presentation of Nexus Authorization Logic[35] (NAL) can formally be said to be lax and in particular can beembedded in the logic S4 [16]. Intuitively, the lax interpretationallows a more liberal ascription of beliefs to principals. Formally,a lax system includes the axiom X .X A Says X (whereas in
CCS ’19, November 11–15, 2019, London, United KingdomProof Derivation RulesSyntaxF, G, HSkalka et al.:: f (t, .)truefalseF Says FXF FF FF F X .F X .FTrue true -IntroL G F GAssume , F F -IntroR F F G -Intro FX fv( ) X .FUnit F , F A Says G A Says G A Says F -Elim F G -Elim X .F F [G/X ] -Intro , F G F GBind A Says F , F H H -Intro F G F G , G H -Intro F [G/X ] X .F -Elim X .F -Elim F G G -ElimL F G F F -ElimR F G G , F GX (fv( ) fv(G)) GFigure 2: NALlight syntax and proof derivation rules.a non-lax system we can only deduce X A Says X if X is atheorem). While the lax interpretation of Says has been assumedby other systems, various authors have suggested that it can leadto dangerous consequences [1, 17, 19]. This includes the authors ofa more recent version of Nexus Authorization Logic, called FOCAL,who refer to the lax interpretation of Says in NAL as a “bug” [19]. Athorough formal study of lax vs. non-lax interpretations identifiesthe core issue as the axiom of escalation [3] which results fromextending classical logic with a lax interpretation of Says: X , Y .(A Says X ) (X A Says Y )However, since NAL is not classical—in particular it lacks negationand the law of excluded middle—it does not exhibit escalation. Furthermore, it enjoys the properties of Says transparency and handoff,which are desirable in any authorization logic. The former meansthat any principle can be trusted to assert their own worldview,whereas the latter supports delegation of authority in distributedsettings. The use of NAL also has implementation benefits—laxlogic can be interpreted monadically, and a monadic interpretation of Says readily supports a Curry-Howard isomorphism withtyped monadic structures in a functional calculus (as we show inSection 2.1.4).1 Thus terms in the calculus can constitute proof witnesses, which enables optimization techniques (e.g., certain typesof reduction).Another important point is that in a proof checking system, beliefs relevant to a judgment are explicitly provided as a componentof the judgment. And in the PCNC implementation (see Section 5.1),beliefs provided to support a proof are always cryptographicallysigned and thus ascribed to a principal (i.e. the signer). Therefore,problems with “importing beliefs” as a consequence of laxity notedby Hirsch et al. [19] are ameliorated in our setting. For these reasons,in PCNC we build on NAL.2.1.2 Syntax and Proof Theory of NALlight . In Figure 2 we presentthe syntax and proof theory of the logic NALlight in a judgmentalstyle. The logic NALlight is a simplified fragment of NAL with astreamlined set of atomic principals A rather than the more complex principals used by Schneider et al. [35]. These principals areencoded using a subset of nullary atomic formulas (rather thanintroducing a new
jmk@cs.rit.edu Sahil Gupta Rochester Institute of Technology Rochester, NY, USA sg5414@rit.edu Kyle Diller Rochester Institute of Technology Rochester, NY, USA kid6584@rit.edu Steffen Smolka Cornell University Ithaca, NY, USA smolka@cs.cornell.edu Nate Foster Cornell University Ithaca, NY, USA jnfoster@cs.cornell.edu ABSTRACT Computer networks often serve as the first line of defense against .
since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARKS: ITALIAN PROOF MARKS, cont. ITALIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1951 Brescia provisional proof for all guns since 1951 Gardone provisional proof for all guns
PROOF MARKS: BELGIAN PROOF MARKSPROOF MARKS: BELGIAN PROOF MARKS, cont. BELGIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1852 Liege provisional black powder proof for breech loading guns and rifled barrels - Liege- double proof marking for unfurnished barrels - Liege- triple proof provisional marking for
2154 PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARK CIRCA PROOF HOUSE TYPE OF PROOF AND GUN since 1950 E. German, Suhl repair proof since 1950 E. German, Suhl 1st black powder proof for smooth bored barrels since 1950 E. German, Suhl inspection mark since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont.
PROOF MARKS: GERMAN PROOF MARKSPROOF MARKS: GERMAN PROOF MARKS, cont. GERMAN PROOF MARKS Research continues for the inclusion of Pre-1950 German Proofmarks. PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1952 Ulm since 1968 Hannover since 1968 Kiel (W. German) since 1968 Munich since 1968 Cologne (W. German) since 1968 Berlin (W. German)
Carrying capacity is typically expressed as the number of animals of a certain type which can be supported in an ecosystem. Carrying capacity may be seen as an equilibrium or balance. However, the carrying capacity for many species is always changing due to various factors. The carrying ca
THE CONCEPT OF CARRYING CAPACITY The question of how much public use can ultimately be accommodated in a national park or related area is often framed in terms of carrying capacity. Indeed, much has been written about the carrying capacity of national parks. The underlying concept of carrying capacity has a rich history in the natural resource .
We present a textual analysis of three of the most common introduction to proof (ITP) texts in an effort to explore proof norms as undergraduates are indoctrinated in mathematical practices. We focus on three areas that are emphasized in proof literature: warranting, proof frameworks, and informal instantiations.
and Proof Chapter 2 Notes Geometry. 2 Unit 3 – Chapter 2 – Reasoning and Proof Monday September 30 2-3 Conditional Statements Tuesday October 1 2-5 Postulates and Proof DHQ 2-3 Block Wed/Thurs. Oct 2/3 2-6 Algebraic Proof DHQ 2-5 UNO Proof Activity
