Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://lvk.cs.msu.su/~sveta/lecture1_formal_methods.pdf Äàòà èçìåíåíèÿ: Thu Dec 3 15:50:08 2015 Äàòà èíäåêñèðîâàíèÿ: Sat Apr 9 22:38:50 2016 Êîäèðîâêà:

. ..-.. ..


:
Qadir, J.; Hasan, O., Applying Formal Methods to Networking: Theory, Techniques, and Applications, Communications Surveys & Tutorials, IEEE , vol.17, no.1, pp.256-291, 2015

03.12.2015

. ..-.. ..

2



· ­ , , · ­ · ­ ,
03.12.2015 . ..-.. .. 3



· ( ) ­ · ­ · ­
03.12.2015 . ..-.. .. 4




! !



03.12.2015

. ..-.. ..

5


(1981)
: want1 = false, want2 = false, turn = 1
1: while (true) { want1 := true; turn := 1; while want2 and turn = 2 do { }; want1 := false; }
03.12.2015



2: while (true) { want2 := true; turn := 2; while want1 and turn = 1 do { }; want2 := false; }
6

. ..-.. ..


(1981)

want1 := false 1CS want1 := true 1W1 turn := 1 1W2

1NCS

not (want2 = true and turn = 2) want2 := false 2CS want2 := true 2W1 turn := 2 2W2

2NCS

not (want1 = true and turn = 1)
03.12.2015 . ..-.. .. 7


(1981)


· (safety)
Reachability analysis , ¬(1 2)

· (liveness)
Loop detection 1 1 (2 2)
03.12.2015 . ..-.. .. 8


(1981)


·
?

03.12.2015

. ..-.. ..

9


vs.


03.12.2015

. ..-.. ..

10


vs.
--

03.12.2015

. ..-.. ..

11



·


·


03.12.2015

. ..-.. ..

12



·


·


·
­
03.12.2015 . ..-.. .. 13



· · · · · · ·
. ..-.. .. 14

03.12.2015



·


·


·

03.12.2015 . ..-.. .. 15



· · · · · · · Mu-
. ..-.. .. 16

03.12.2015



·


·
Theorem proving

·
Model checking
03.12.2015 . ..-.. .. 17



" " · ·

: · ·
03.12.2015 . ..-.. .. 18



· Formal methods have not yielded results commensurate with the effort to use them. They are overblown, verbose, hard to use, hard to understand. Vint Cerf · We reject: kings, presidents and voting. We believe in: rough consensus and running code. David Clark
03.12.2015 . ..-.. .. 19



T

· · · · · · ·

David Clark he Design Philosophy of the DARPA Internet Protocols SIGCOMM '88. -- ACM, 1988. -- Pp. 106­114.
. ..-.. .. 20

03.12.2015




. ..-.. ..

03.12.2015

21



: · Deadlocks - , · Livelocks ­ · Improper termination ­ ­ !
03.12.2015 . ..-.. .. 22


Reachability Analysis
· · · · · : Black Holes ­ Fowrarding Loops ­ ?

! ?
03.12.2015 . ..-.. .. 23


Network Security
: · · ·

03.12.2015

. ..-.. ..

24



· · ·
03.12.2015 . ..-.. .. 25


­

. ..-.. ..

03.12.2015

26



Andreas Voellmy, Paul Hudak Nettle: taking the sting out of programming network routers
Andreas Voellmy, Hyojoon Kim, Nick Feamster Procera: a language for high-level reactive network control Joshua Reich , Christopher Monsanto , Nate Foster , Jennifer Rexford , David Walker Modular SDN Programming with Pyretic
03.12.2015 . ..-.. .. 27


Control Plane Verification

03.12.2015

. ..-.. ..

28



APP3
API OpenFlow API
03.12.2015 . ..-.. .. 29

APP4

APP2


APP1



API

APP4

APP2

APP3

APP1


OpenFlow API
03.12.2015 . ..-.. .. 30





from pyretic.lib.corelib import * # def main(): return flood() # 10.0.0.1 def access_control(): return ~(match(srcip='10.0.0.1') | match(dstip='10.0.0.1'))
03.12.2015 . ..-.. .. 31


Control Plane Verification
Marco Canini, Daniele Venzano et. all A NICE way to test OpenFlow applications Thomas Ball, Nikolaj Biorner et all. VeriCon: Towards Verifying Controller Programs in Software-Defined Networks
03.12.2015 . ..-.. .. 32


Data Plane Verification
· · ­ ·

03.12.2015

. ..-.. ..

33




· · · · · · · DPI A B , B A · R, ­ T



Al-Shaer E., Al-Haj S. FlowChecker: Configuration Analysis and Verification of Federated Openflow Infrastructures // SafeConfig '10. -- Chicago, USA, 2010. -- Pp. 37­44.

B

A
Kazemian P., Chang M., Zeng H., Varghese G., McKeown N., Whyte S. Real Time Network Policy Checking Using Header Space Analysis // NSDI'13. -- Lombard, USA, 2013. -- Pp. 99­111.


VERMñNT VERifying MONiTor
VERMONT







· · ·







State 1: Header h1 Port #1 Switch #1 State 2: Header h2 Port #1 Switch #2 State 3: Header h3 Port #1 Switch #3

h2 h1

h3 h4

B
State 4: Header h4 Port #2 Switch #3

A :
1. 2. 3.
Switch Port Header

{0, 1}m {0, 1}l {0, 1}k





/
( , )
Switch Port


( , )
Switch Port Switch Port


( )
Port Header Port Header


( , )
Switch Port Header Switch Port Header





OpenFlow Pattern Rewrite
* - Pattern,
P[0] H[0]
x1 x2 x3 x4

H[1]

H[2]

H[3]

Pattern Rewrite

0001 0001

011* 110*
y1 y2 y3 y4

0001 0001

**** ****

0001 0001

* - Rewrite
39


Binary Decision Diagram (ROBDD)
1 1 2 3 4
2

1

BDD
1 2 3
4

1
2

3

4

011* 1 2 3 4 110* 1 2 3 4

2
3

3 4
4

1 1 2 2 (33 )(4 4 4 4)

4

0

1

0

1


BDD
· BDD , · BDD FlowTable · BDD
· BDD

· BDD ·
·

·



41




,
x[field] = const x[field] = y[field] ¬ . . + [,]

1 , = (, ) , = : -1 , , [i,j] , = , , + ( , ) = 1, (, ) () ( ) ( , ) + (, )


:
aux: lead_to_cycle(x) := In(x) and Exist[y: R_tc(x,y) and Exist[z: R_tc(y,z) and y == z ] ]; x

z y

main: no_state_cycles () := Forall[x: not lead_to_cycle (x)];



<=> ,
BDD A B P











,

1.094 6.294

OBDD, . . OBDD


18.028 642 18 0.043 0.047 0.855 2.013 3.764

+




,

Stanford University Backbone Network



90 Mb Fat Tree 16 757000 48


Stanford network verification




()

<= 3 <= 4 . / . . / .

-

3043.687 166.191 174.845 293.522 736.015 1 0 0 / 0 .3 * 70 / 1*

YES NO NO YES
-






Feeder

?

-



: ­ ­





VERMONT , ,



VERMONT
2013

() () 3100 37000 >4000 1000 400000 1200000 100 - 600 2 - 1000 68 - 100 0.1 ??? 350 - 67000


FO[TC] C TL

OpenFlow


NetPlumber
Stanford Uni ve rsi ty

2013

VeriFlow
Uni ve rsi ty of Il l i noi s

2013

C TL

AP Verifier
Uni ve rsi ty of Te x as

2013

Anteater
Uni ve rsi ty of Il l i noi s




2011

FlowChecker
Uni ve rsi ty of North Carol i na

2010


VERMONT
Network disjoint
Port #02

Port #03

h2 h3 s1
Port #01

h1

Port #04

h4



main: disjoint() := Forall[x, out_x, y, out_y: !R(x, out_x) or !R(y, out_y) or x[p] == out_y[p] and out_x[p] == y[p] or x[p] == y[p] and out_x[p] == out_y[p] ]; y out_y x out_x



main: disjoint() := Forall[x, out_x, y, out_y: !R(x, out_x) or !R(y, out_y) or x[p] == out_y[p] and out_x[p] == y[p] or x[p] == y[p] and out_x[p] == out_y[p] ]; y out_y x out_x


MININET simulator CLI

There are more components whose output is not shown: · SDN controller · VERMONT Verifier · VERMONT Feeder

VERMONT proxy CLI

Switch S1 is already connected to VERMONT proxy

Rules at switch S1

Flow table of switch S1 is currently empty


Rules at switch S1

VERMONT proxy CLI

MININET simulator CLI

Setting VERMONT proxy to interrupt mode


MININET simulator CLI

Host h1 starts to ping host h3

VERMONT proxy CLI

Controller tries to install the rules to transmit ping packets Proxy interrupts command from the controller and sends them to Verifier Verifier create an updated model of the data plane and checks them against a set of PFPs

Rules at switch S1


MININET simulator CLI

First packet of the flow uses slow path

VERMONT proxy CLI

Rules at switch S1

Proxy delivers verified commands to the switch Switch table contains rules to transmit packets between host h1 and host h3


MININET simulator CLI

Subsidiary packets use fast path

VERMONT proxy CLI

Rules have an idle timeout and will expire in 5 seconds

Rules at switch S1


MININET simulator CLI

Host h2 starts to ping host h4

VERMONT proxy CLI

Controller tries to install the rules to transmit ping packets Proxy interrupts command from the controller and sends them to Verifier Verifier create an updated model of the data plane and checks them against a set of PFPs

Rules at switch S1


VERMONT proxy CLI

MININET simulator CLI

Proxy drops unsafe commands and notifies the controller

Rules at switch S1


MININET simulator CLI

Why does ping work?

VERMONT proxy CLI

Packets are delivered through the control plane We can block them! But do we really want to?

Rules at switch S1


MININET simulator CLI

Packets start to use fast path

VERMONT proxy CLI

Old rules have been expired Controller is allowed to install new rules
Switch table contains rules to transmit packets between host h2 and host h4

Rules at switch S1


MININET simulator CLI

Packets use slow path

VERMONT proxy CLI

Rules to transmit packets from host h1 to host h3 violate forwarding policy

Rules at switch S1


MININET simulator CLI

Packets start to use fast path

VERMONT proxy CLI

Switch table contains rules to transmit packets between host h1 and host h3

Rules at switch S1



· · 0 , +1 = 0 , 1 , ... , , +1 , ... · ( ) ­
03.12.2015 . ..-.. .. 64



· ­
,

· - , · = 1 , ... , , ( ) = (... , 1 ... )
03.12.2015 . ..-.. .. 65



· : , · ­ , (, ).



: · C0 · - , . : · , , : 1. 0 2. = 0



, · A. Noyes, T. Warszawski, P. Cernyand, N. Foster. Toward Synthesis of Network Updates. 2-nd Workshop on Synthesis (CAV-2013), 2013, Saint Petersburg, Russia


-
· · · · Post-condition (X): = Invariant (X) : ( ( , ( , (0 )))



· M. Reitblatt, N. Foster, J. Rexford, D. Walker. · Consistent updates for software-defined networks: change you can believe in! · HotNets, v. 7, 2011.


-
· · · · Post-condition (X): = 0 { 0 } { 1 } Invariant (X) : 0 0 0 1

S. Raza, Y. Zhu, C.-N. Chu S. Raza, Y. Zhu, C.-N. Chuah. Graceful network state migrations. IEEE/ACM Transactions on Networking, v. 19, N 4, 2011.



· - (X): · = · (X) :
· 0 0 ( )

· 0 · ­ 0



· · · · · - (X): () = () (() = () ()) . (X) : () = (),

· K. Kogan, S. Nikolenko, W. Culhane, P. Eugster, E. Ruan. Towards efficient implementation of packet classifiers. Proc. of the 2-d Workshop on Hot Topics in SDN, 2013.




h

( h, 1 )

( h, 1 )

( h, 1 )

h




( h, 2 ) h ( h, 1 )

( h, 2 )

( h, 2 )
( h, 1 )

( h, 2 )

h h

(h,1)

3- 1:




(h,2)
h

( h, 2 )

( h, 2 )

( h, 2 )
( h, 1 )

( h, 2 )

h h

(h,1)

3- 1: 2:




(h,2)
h

( h, 2 )

( h, 2 )

( h, 2 )

( h, 2 )

h

3 1 2 3

- : : :




03.12.2015

. ..-.. ..

85