I nte rna t io na l J o urna l o f   E lect rica l a nd   Co m p ute E ng in ee ring   ( I J E CE )   Vo l.   9 ,   No .   4 A u g u s t   201 9 ,   p p .   2 6 2 7 ~2 6 3 6   I SS N:  2 0 8 8 - 8708 DOI : 1 0 . 1 1 5 9 1 / i j ec e . v9 i 4 . p p 2 6 2 7 - 2636          2627       J o ur na ho m ep a g e h ttp : //ia e s co r e . co m/ jo u r n a ls /in d ex . p h p / I JE C E   A VN m o deling   a ppro a ch f o r veri ficatio n pur po ses       G ui do   M a r chet t o ,   Ricc a rdo   Sis t o   M a t t e o   Virg ilio ,   J a lo ll idd in Y us up o v   De p a rtme n o f   Co n tr o a n d   Co m p u ter E n g in e e ri n g ,   P o li tec n ico   d T o rin o ,   Italy       Art icle  I nfo     AB ST RAC T     A r ticle  his to r y:   R ec eiv ed   A p r   27 ,   2 0 1 8   R ev i s ed   J an   2 8 ,   2 0 1 9   A cc ep ted   Mar   4 ,   2 0 1 9       Ne tw o rk   F u n c ti o n   V irt u a li z a ti o n   (NF V a rc h it e c tu re a re   e m e rg in g   to   in c re a se   n e t w o rk s   f l e x ib il it y .   H o w e v e r,   th is  re n e w e d   s c e n a rio   p o se n e c h a ll e n g e s,  b e c a u se   v irt u a li z e d   n e tw o rk s,   n e e d   to   b e   c a re f u ll y   v e ri f ied   b e f o re   b e in g   a c tu a ll y   d e p lo y e d   in   p ro d u c ti o n   e n v iro n m e n ts  in   o rd e t o   p re se rv e   n e tw o rk   c o h e re n c y   (e . g . ,   a b se n c e   o f o rwa rd in g   lo o p s ,   p re se rv a ti o n   o f   se c u rit y   o n   n e tw o rk   tra ff ic,  e tc.).   No w a d a y s,  m o d e c h e c k in g   to o ls,  S AT  so lv e rs,  a n d   T h e o re m   P ro v e rs  a re   a v a il a b le  f o f o rm a v e ri f ica ti o n   o f   su c h   p ro p e rti e in   v irt u a li z e d   n e tw o rk s.  Un f o rtu n a tely ,   m o st  o f   th o se   v e rif ic a ti o n   to o ls   a c c e p t   in p u t   d e sc rip t io n w rit ten   in   sp e c if ica ti o n   lan g u a g e th a a re   d if f icu lt   to   u se   f o p e o p le  n o e x p e rien c e d   in   f o rm a m e th o d s.  A ls o ,   in   o rd e r   to   e n a b le  th e   u se   o f   f o rm a v e ri f ica ti o n   to o ls  in   re a sc e n a rio s,  v e n d o rs  o f   V irt u a Ne tw o rk   F u n c ti o n (V N F s)   sh o u ld   p ro v id e   a b stra c m a th e m a ti c a l   m o d e ls  o f   th e ir  f u n c ti o n s,  c o d e d   i n   t h e   sp e c if ic  in p u t   lan g u a g e o f   th e   v e ri f ica ti o n   to o ls.   T h is  p r o c e ss   is  e rro r - p r o n e ,   ti m e - c o n su m in g ,   a n d   o f ten   o u tsi d e   th e   V NF  d e v e lo p e rs’  e x p e rti se .   T h is  p a p e p re se n ts  a   f ra m e w o rk   th a w e   d e si g n e d   f o a u to m a ti c a ll y   e x trac ti n g   v e ri f ica ti o n   m o d e ls  sta rti n g   f ro m   a   Ja v a - b a s e d   re p re se n tatio n   o f   a   g iv e n   V NF.   It  c o m p rise s   a   Ja v a   li b ra ry   o c las se to   d e f in e   V NFs  in   a   m o re   d e v e lo p e r - f rien d ly   wa y ,   a n d   a   to o to   tran sla te  V NF   d e f in it io n in t o   f o r m a v e rif ic a ti o n   m o d e ls  o f   d iff e r e n t   v e ri f ica ti o n   to o ls.   K ey w o r d s :   F o r m al  v er i f icatio n     M o d el  ex tr ac tio n     M o d elin g       N et w o r k   f u n ctio n s   P ar s er   Co p y rig h ©   2 0 1 9   In stit u te o A d v a n c e d   E n g i n e e rin g   a n d   S c ien c e   Al rig h ts re se rv e d .   C o r r e s p o nd ing   A uth o r :   J alo llid d in   Yu s u p o v ,   Dep ar t m en t o f   C o n tr o l a n d   C o m p u ter   E n g i n ee r i n g ,   P o litecn ico   d T o r in o ,   C o r s o   Du ca   d eg li  A b r u zz i,  2 4 ,   T O,   I taly .   +3 9   3 4 5   5 1 7 0 7 5 3 .   E m ail:  j alo llid d in . y u s u p o v @ p o lito . it       1.   I NT RO D UCT I O N   T h telec o m m u n ica tio n s   w o r ld   is   ex h ib it in g   v er y   r ap id   ch an g in   i ts   v ar io u s   asp ec t s   s u c h   as   s er v ice  f le x ib ilit y ,   ar ch i tectu r al  d esig n ,   a n d   th w a y   s er v ic es  ar cr ea ted ,   s o u r ce d ,   d ep lo y ed ,   an d   s u p p o r ted .   Ne w   s t u d ies  i n   th is   s ec to r   ar co m i n g   o u e v er y   d a y   to   ch an g t h en t ir s tr u ct u r e   o f   th s y s te m   b y   i n tr o d u ci n g   d y n a m ic   ad j u s t m e n o f   th e   n et w o r k   r eso u r ce s ,   c u s to m   co n f i g u r atio n   o n   p er - u s er   b asi s ,   n e t w o r k   p r o g r am m ab ilit y ,   etc.   T h ex p ec tatio n   f o r   s i g n i f ican co s t   s av i n g s   i s   f r eq u en tl y   m e n ti o n ed   as  o n o f   th e   p r im ar y   b en e f its   o f   th e s s t u d i es.   T h v ir tu a lizat io n   tec h n o lo g y   h as  e m er g ed   a s   w a y   to   d ec o u p le  s o f t w ar ap p licatio n s   f r o m   t h e   u n d er l y in g   h ar d w ar an d   e n a b le  s o f t w ar to   r u n   i n   v ir t u a lized   en v ir o n m e n t,  w it h   co n s eq u en in cr ea s o f   th s er v ice   f lex ib ili t y .   I n   p ar ti cu lar ,   t h n o tio n   o f   Ne t w o r k   Fu n ctio n s   V ir tu aliza tio n   ( N F V)   [ 1 ]   is   e v o lv i n g   to   r e m ed y   t h s tatic   n at u r o f   tr ad itio n al  n et w o r k s   b y   p r o m o tin g   in n o v at io n   i n   n et w o r k   m a n ag e m e n a n d   d ep lo y m en o f   n et w o r k   s er v ices.  I n   an   NFV  en v ir o n m e n t,  n et w o r k   is   co m p r is ed   o f   s o f t w ar e - b ased   ap p licatio n s   c alled   V ir tu al   N et w o r k   F u n c tio n s   ( VNF)   t h at   tak o n   t h r esp o n s ib ilit y   o f   h an d li n g   s p ec i f ic   n et w o r k   f u n c tio n s   th a r u n   o n   o n o r   m o r v ir tu al  m ac h i n e s   ( VM s )   o r   in   co n tai n er s ,   o n   to p   o f   th p h y s ical   n et w o r k i n g   in f r astr u ct u r e.   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 A u g u s t 2 0 1 9   :   2 6 2 7   -   2636   2628   T h id ea   th at  n o w   al m o s an y o n ca n   in tr o d u ce   co m p l ex   VNF  s o f t w ar e,   in   to d ay s   m o d er n   n et w o r k s ,   in cr ea s e s   th i m p ac o f   p o s s ib le  n et w o r k   co n f ig u r atio n   er r o r s .   A s   r es u lt,  s u b s tan t ial  a m o u n o f   ef f o r is   r eq u ir ed   to   en s u r n e t w o r k s   co r r ec tn ess ,   s a f et y ,   an d   s ec u r it y .   T h er ef o r e,   v er if ica tio n   o f   n et w o r k s   is   k e y   to   eli m i n ate  er r o r s   an d   b u i ld   r o b u s t in f r astru ct u r es.  W it h   th is   r esp ec t,  m ec h a n ized   f o r m al  tech n iq u es  h a v p r o v ed   to   b p o w er f u e n g i n es  f o r   f o r m al  v er if ica tio n   o f   t h n et w o r k   b eh a v io r   in   m an y   d if f er e n t   co n tex t s   [ 2 - 4 ] .   I n   th n e t w o r k in g   p an o r a m a,   m o s ex i s ti n g   v er if icatio n   to o ls   -   m o d el  ch ec k in g ,   S A T   s o lv er s ,   an d   th eo r e m   p r o v er s   -   r el y   o n   f o r m al  m o d el  p r o v id ed   ac co r d in g   to   g i v e n   d escr ip tio n   l an g u a g e.   T h m ai n   ch alle n g e   p r o v id er s   o f   N FV   s o f t w ar h a v to   f ac i n   o r d er   to   en ab le   f o r m a v er if ica tio n   o f   v ir t u alize d   n et w o r k s   is   t h m o d el  co n s tr u ctio n t h er is   lar g s e m a n ti g ap   b et w ee n   t h ar ti f ac ts   p r o d u ce d   b y   s o f t w ar e   d ev elo p er s   an d   th o s ac ce p ted   b y   cu r r en v er i f icatio n   to o ls .   Fo r   ex a m p le,   p o w er f u ap p r o ac h es  s u c h   a s   [ 2 ]   an d   [ 5 ]   h a v alr ea d y   e v o l v ed   f r o m   r esear ch   a n d   ar n o w   b ei n g   r o lled   in to   p r o d u ctio n ,   b u th is   g ap   m i g h b a   s ig n i f ica n h u r d le  f o r   th eir   w i d ad o p tio n   in   r ea n et w o r k   e n v ir o n m en ts .   I n   ess e n ce ,   th e s to o ls   ar b ased   o n   a   co m p le x   m o d elin g   tec h n iq u e,   ten d   to   lo ck   th e   u s er   in to   s in g le  k i n d   o f   c h ec k i n g   tech n o lo g y ,   r eq u ir to   ac cu r atel y   m o d el  n et w o r k   f u n ctio n alit y ,   w h ic h   r elies  o n   ex p er in p u t,  an d   u s u all y   o b lig d ev elo p er s   to   lear n   w h o le  n e w   la n g u a g ( e. g . ,   SE FL   i n   [ 5 ] ) .   T h is   m o ti v ate s   t h w o r k   p r esen ted   i n   t h is   p ap er ,   i.e . ,   f r a m e w o r k   f o r   u s er - f r ien d l y   V NF  m o d eli n g   th at  d ev e lo p er s   ca n   u s to   p r o v id f o r m al  d escr ip tio n   o f   t h eir   f u n ctio n s   to   b u s ed   in   v er if icatio n   p r o ce s s .   T h m aj o r   h ig h li g h t o f   o u r   f r a m e w o r k   i s   its   s i m p lici t y   a n d   w d ev elo p   it tar g e tin g   t h r ee   s p ec if ic  o b j ec tiv es:    -   T o   s i m p li f y   t h d ef i n itio n   o f   a   n et w o r k   f u n ctio n   f o r w ar d in g   m o d el  i n   w ell - k n o w n   lan g u a g e.     -   T o   leav s o m g en er al  co n ce p ts   an d   f le x ib ilit y   to   d ev elo p er s   in   s u ch   a   w a y   th a t h e y   c o u ld   d ef i n t h d esire d   b eh av io r   f o r   all  th eir   n et w o r k   f u n ct io n s .     -   T o   p r o v id an   au to m atic  tr an s latio n   f r o m   t h f u n c tio n   m o d e d ef in itio n   in to   an   ab s tr ac f o r m al  m o d el  f o r   v er if ica tio n   to o ls .   I n   o r d er   to   m ee t h ab o v e - m en tio n ed   p r in cip le s ,   w s elec t   J av as  w ell - k n o w n   a n d   w id s p r ea d   lan g u a g th a d ev e lo p er s   f i n d   s i m p le  a n d   ea s y   to   g r a s p .   T h s p ec if ic  lib r ar y   w p r o p o s in   th is   J av a - b ased   f r a m e w o r k   r ep r esen ts   t h t y p ical  s et  o f   h i g h - le v el  o p er atio n s   co m m o n l y   u s ed   f o r   d escr ib in g   t h n e t w o r k   f u n ctio n s   b eh a v io r .   Star tin g   f r o m   s k ele to n   clas s   d ef i n it io n   o f   g e n er ic  n et w o r k   f u n ctio n ,   VNF  d ev elo p er   ca n   ea s il y   e x te n d   th p r o v id ed   ar tif ac ts   to   in h er it  b asic  p r o p er ties ,   d ata  ty p es,  an d   m et h o d s   an d   cu s to m ize   f u n ctio n   b eh a v io r .   Ou r   f r a m e w o r k   also   i n cl u d es  p ar s er   t h at  an al y ze s   th e   J av s o u r ce   co d an d   p r o d u ce s   an   ab s tr ac f o r m al  m o d el  o f   t h n et w o r k   f u n ctio n   t h at  ca n   b au to m at icall y   tr an s lated   in to   t h in p u la n g u a g e   p r o p er   o f   g iv en   v er i f icatio n   to o l.  T h is   s ec o n d   s tep   is   clea r l y   to o d ep en d en an d   w e   p lan   to   en r ich   o u r   f r a m e w o r k   in   o r d er   to   s u p p o r th v as t   m aj o r it y   o f   th e x is t in g   to o ls .   C u r r en tl y ,   th p ar s er   o p e r atio n   is   o r ien ted   to   f o r m al  v er i f ica tio n   to o ls   b ased   o n   th a n al y s i s   o f   l o g ic  f o r m u las  an d   in   p ar ticu lar   th Ver iGr ap h   [ 6 ]   to o is   ad o p ted   as  u s ca s e.   Ver ig r ap h   r eq u ir es  to   m o d el  co m p lex   n et w o r k   s ce n ar io s   a s   s ets  o f   First   Or d er   L o g ic  ( F OL )   f o r m u la s   a n d   u s es   an   S MT   s o lv er ,   Z 3 [ 7 ] ,   to   v er i f y   s atis f iab ilit y   o f   t h es e   f o r m u las.   W h e n ce   d e v elo p ed   tr an s lato r   f o r   co n v er ti n g   t h o u tp u t   o f   th e   p ar s er   to   t h e   p r o p er   s et  o f   FO L   f o r m u las.   T o   ch ec k   th e   co r r ec tn es s   o f   t h m o d els  o b tai n e d ,   th d e v elo p er   ca n   r u n   te s t s   to   v er if y   n et w o r k   p r o p er ties   in   ter m s   o f   r ea ch ab ilit y   b et w ee n   d i f f er e n n o d es  in   s ev er al  s i m p le  g r ap h s   th at  i n clu d t h d ev elo p ed   VNF  m o d el.   W f ir s in tr o d u ce   o u r   m o d eli n g   tech n iq u i n   Sec tio n   3 .   T h u s ca s an d   t h e   o b tain ed   r esu lt s   ar p r esen ted   in   Sec tio n   4 .   I n   ad d itio n ,   Se ctio n   2   d is cu s s e s   r elate d   w o r k ,   w h ile  Sect io n   5   co n clu d es t h p ap er .       2.   RE L AT E WO RK   T h er h as  b ee n   s ig n i f ica n a m o u n o f   ac ti v it y   i n   t h p ast  y ea r s   o n   atte m p t in g   to   p r o v id p r o p er   s u p p o r f o r   th e   tr an s latio n   o f   s o f t w ar s y s te m   d escr ip tio n s   t o   th i n p u m o d els  f o r   v er i f ic atio n   to o ls .   Am o n g   th o th er s ,   w ca n   m e n tio n   B an d er [ 8 ]   an d   J av aP ath Fin d er   [ 9 ] .   T h t w o   ap p r o ac h es  ar b ased   o n   m o d el   ch ec k i n g ,   an d   th m o d els  th e y   e x tr ac ar m o d els  o f   J av s o f t w ar e.   T h m ai n   d if f er e n ce   w it h   r esp ec to   th e   p r o p o s ed   f r a m e w o r k   is   t h at  th e y   co n s id er   g e n er al - p u r p o s J av p r o g r am s   a n d   th eir   m ai n   tar g et  i s   t h e   id en ti f icatio n   o f   p r o g r a m m i n g   er r o r s   an d   b u g s .   Her i n s tead   w d ea w i th   t h f o r w ar d i n g   b eh av io r   o f   VN Fs .   W ar n o in ter ested   in   all  th d etails  o f   th VNF  co d ex ec u tio n .   F u r th er m o r e,   w w an t   o u r   an al y s i s   to   b e   ex tr e m e l y   f ast.   Mo r eo v er ,   m a n y   ap p r o ac h es  a n d   m et h o d s   f o r   s tatic  n et w o r k   an al y s is   h av b ee n   p r o p o s ed   [2 ,   5 ,   1 0 ] .   Net w o r k   Op ti m ized   Data lo g   [ 2 ]   r elies  o n   Data lo g   b o th   f o r   n et w o r k   m o d els  an d   p o licy   co n s tr ain ts .   B UZ Z   [ 1 0 ]   u s es h a n d - g e n er at ed   m o d els o f   n et w o r k   f u n ctio n s   in   d o m ai n   s p ec i f ic  la n g u a g e.   A s   w d i s cu s s ed   ea r lier ,   m o d elin g   n e t w o r k   f u n ctio n alit y   f o r   u s in g   th e s to o ls   is   d if f ic u lt  a n d   r eq u ir es  d etailed   u n d er s ta n d in g   o f   th v er i f icatio n   to o l’ s   s e m an tics .   T h er ef o r e,   o u r   au to m ated   ap p r o ac h   to   g en er ate  m o d els  eli m i n ate s   Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2 0 8 8 - 8708       A   V N F   mo d elin g   a p p r o a c h   fo r   ve r ifica tio n   p u r p o s es ( Gu id o   Ma r ch etto )   2629   th n ec es s it y   o f   h av in g   d etai l ed   d o m ai n   k n o w led g e   an d   h e lp s   n e t w o r k   e n g in ee r s   to   q u i ck l y   d eter m i n e   th e   b eh av io r   o f   n et w o r k   f u n ctio n .   On   th o t h er   h an d ,   S y m Ne [ 5 ]   co n s tr u cts  m o d els  u s i n g   an   i m p er ati v e,   m o d elin g   la n g u ag e,   ca lled   S y m b o lic  E x ec u tio n   Frie n d l y   L a n g u a g ( SEF L ) .   W h ile   th w a y   t h is   la n g u a g h a s   b ee n   d esig n ed   h a s   s i m ilar ities   w it h   th J a v ab ase d   lib r ar y   w p r o p o s e,   th is   ap p r o ac h   lack s   t h id ea   o f   ea s o f   m o d eli n g ,   b y   in tr o d u ci n g   n e w   la n g u a g e.   Desp ite  th f ac t h at  t h e y   p r o v id p ar s er s   to   au to m a tic all y   g en er ate  SE F L   m o d el s   f r o m   r ea n et w o r k   f u n ctio n s ,   t h is   g en er atio n   o n l y   co v er s   r o u ter s   a n d   s w itc h es.  O u r   ap p r o ac h ,   in s tead ,   is   b ased   o n   th w ell - k n o w n   u s er - f r ie n d l y   J av la n g u a g an d   ca n   b u s ed   to   v er i f y   a n y   v ir t u al  n et w o r k   f u n ctio n .   p r o p o s al  m o r s i m ilar   to   o u r   ta r g et   is ,   NFacto r   [ 1 1 ] ,   w h ich   p r o v id es  a   s o l u tio n   to   a u t o m a ticall y   an al y ze   t h s o u r ce   co d o f   g iv e n   n et w o r k   f u n ctio n   to   g e n er ate  an   ab s tr ac f o r w ar d in g   m o d el,   m o ti v ated   b y   n et w o r k   v er if icat io n   ap p licati o n s .   W h ile  r el y in g   o n   ad v a n ce d   to o ls   [ 1 2 ]   an d   tech n i q u e s   [ 1 3 ,   1 4 ]   f r o m   th e   p r o g r am   a n al y s i s   co m m u n it y ,   th e y   d o   n o r eq u ir s p ec i f ic  s tr u ct u r o f   t h s o u r ce   co d o f   th f u n ctio n   to   b e   an al y ze d .   T h i s   f ea tu r e   is   co n s i d er ed   as  an   ad v an ta g f r o m   g en er ali t y   p o in o f   v ie w .   U n f o r tu n ate l y ,   cr ea ti n g   m o d el  th at  ca p t u r es a ll c o d p ath s   o f   n et w o r k   f u n ctio n   i s   ch alle n g i n g ,   b ec au s th s tate  p r o ce s s in g   m a y   b h id d en   d ee p   in   th co d e.   T h is   m a y   ca u s t h an a l y s i s   to   m is s   ce r tain   s tate  ch a n g e s .   Fo r   ex a m p le,   i m p le m en ta tio n s   m i g h u s p o in ter   ar ith m e tic  to   ac ce s s   s tate  v ar iab le s ,   w h ic h   is   d if f ic u lt  to   tr ac e,   an d   NFacto r   d o es   n o t   s ee m   t o   d ea w it h   t h ese   la n g u a g f ea tu r es  ap p r o p r iatel y .   An o th e r   li m itatio n   o f   th e   ap p r o ac h es  b ased   o n   t h e   ex tr a ctio n   o f   m o d el s   f r o m   s o u r ce   c o d is   t h at  t h co d o f   m o s t   n et w o r k   f u n ctio n s   is   t y p i ca ll y   p r o p r ietar y .   I n s tead   o f   r el y in g   o n   v e n d o r s   to   r elea s t h eir   co d e,   th e   ai m   o f   o u r   f r a m e w o r k   i s   to   g i v d ev elo p er s   th o p p o r tu n it y   to   i m p le m e n t h eir   n et w o r k   f u n ctio n s   r ese m b li n g   as  m u c h   as  p o s s ib le  th r ea o n e’ s   b eh av io r .       3.   M O DE L I N G   T E CH N I Q U E   C u r r en t l y ,   th er i s   n o   s ta n d ar d   o r   m o d elin g   la n g u a g to   ac cu r atel y   r ep r esen t h d i v e r s it y   a n d   co m p le x it y   o f   n et w o r k   f u n cti o n s .   Mo s o f   th r e s ea r ch   e f f o r ts   i n   p r o p o s in g   V NF  m o d els  ar f o c u s ed   o n   n et w o r k   v er i f icatio n   an d   g ai n ed   p o p u lar it y   in   t h v er i f icati o n   co m m u n it y .   I n   t h is   s ec tio n ,   w li s th o p en   p r o b lem s   t h at  w h a v e n co u n ter ed   w h i le  lo o k in g   at  t h p r o p o s ed   VNF  m o d els in   t h v er i f icatio n   co n te x t.     3 . 1 .   O v er v ie w   a nd   pro ble m   s t a t em e nt   Mo d elin g   o f   VNF s   is   u s ef u in   n u m b er   o f   w a y s   r an g in g   f r o m   f i n d in g   s ca lab ilit y   i s s u es  i n   ap p licatio n s   to   f in d i n g   n et wo r k   co n f i g u r atio n   b u g s ,   in   p ar ticu lar   b y   m ea n s   o f   f o r m a v er if icatio n   to o ls .   Ho w e v er ,   f o r m al  m o d eli n g   o f   n et w o r k   f u n ct io n alit ies  i s   d if f ic u lt  a n d   r eq u ir es  d etailed   u n d er s tan d i n g   o f   t h e   s p ec if ic  v er i f icatio n   to o l’ s   in ter n als,  s e m a n tic s ,   an d   m o d elin g   la n g u a g e.   W ith   t h i s   r es p ec t,  an   au to m ated   ap p r o ac h   to   g en er ate  m o d els  e li m i n ate s   th n ec es s it y   o f   h a v i n g   d etailed   k n o w led g in   t h f o r m al  v er i f icatio n   d o m ai n   a n d   h elp s   e n g i n ee r s   to   q u ick l y   d eter m i n t h b eh a v i o r   o f   VNF - b ased   n et w o r k ,   s t ar tin g   f r o m   m o r u s er - f r ie n d l y   d escr ip tio n   o f   th in v o lv ed   VNF s .   I n   p ar ticu la r ,   th p o s s ib ilit y   to   d escr ib e   V NFs   b y   m ea n s   o f   a   J av a - li k m o d eli n g   la n g u a g e   w o u l d   s i g n if ica n tl y   lo w er   b ar r ier s   to   en tr y   f o r   th e s p o w er f u v er if icatio n   ap p r o ac h es.    An   i m p er ati v la n g u a g s u c h   as   J av f o cu s es  o n   d escr i b in g   h o w   a   p r o g r a m   o p er ates.  A   VN F   d ev elo p er   ca n   w r ite  co d th at  d escr ib es  in   ex ac d etail  t h e   s tep s   th at  t h VNF  m u s m a k w h en   p ac k et  i s   r ec eiv ed   f r o m   o n e   o f   its   i n ter f ac es.  I n   co n tr ast,  d ec lar a tiv lan g u ag e s   ad o p ted   in   l o g ic - b ased   f o r m a v er if ica tio n   to o ls   d o   n o t sp ec if y   s tep   o r   s eq u en ce   o f   s tep s   t o   ex ec u te,   b u t r at h er   p r ed icate s   th at  m u s h o ld .     T h co n ce p tu al  g ap   b et w ee n   th e s t w o   r ep r ese n tatio n s   i s   th e   i m p o r tan c h alle n g e   s o l v ed   b y   o u r   ap p r o ac h .   T h p r o p o s ed   f r am e w o r k   p r o v id es  J a v lib r ar y   an d   a   p ar s er .   T h lib r ar y   ca n   b u s ed   f o r   m o d eli n g   n et w o r k   f u n ctio n s   b y   m ea n s   o f   an   i m p er ati v lan g u a g e.   T h p ar s er   th en   au to m atica ll y   g e n er ates   ab s tr ac tio n   m o d els  f r o m   t h ese   d escr ip tio n s .   B asicall y ,   th p a r s er   tak es  as  a n   i n p u t h d ef in itio n   w r itte n   u s i n g   o u r   lib r ar y   a n d   p r o d u ce s   an   ab s tr ac f o r m al  m o d el  d es cr ib in g   t h b e h a v io r   o f   th e   n et w o r k   f u n ctio n .   T h is   g iv e s   th p o s s i b il it y   o f   au to m at icall y   tr a n s la tin g   t h d ef i n itio n   t h at  is   w r itte n   i n   w e ll - k n o w n   lan g u ag e   in to   m o r h ig h - le v el,   d o m ai n - s p ec if ic  co n s tr ai n lan g u ag e ,   th at  w o u ld   b d if f ic u lt  to   d ea w it h   m a n u all y .   T h r est  o f   th is   s ec tio n   p r e s en t s   t h J av lib r ar y   a n d   t h p ar s er   w d ev elo p ed ,   w h ich   s u m   u p   o u r   m o d eli n g   tech n iq u e.     3 . 2 .   O v er v ie w   a nd   pro ble m   s t a t em e nt   T h f r a m e w o r k   p r o v id es  a   l ib r ar y   th at   allo w s   u s er s   to   e asil y   w r ite   m o d els   o f   v ir t u al   n et w o r k   f u n ctio n s .   B y   m ea n s   o f   t h i s   li b r ar y ,   t h u s er   ca n   s i m p l y   d es cr ib th f u n ctio n a lit y   o f   th n et w o r k   f u n ctio n   b y   in s ta n tia tin g   o b j ec ts   o f   th lib r ar y   c lass e s   a n d   b y   ca lli n g   ce r t ain   m eth o d s   t h at  co r r esp o n d   t o   t y p ical  o p er atio n s   p er f o r m ed   i n s id n et w o r k   f u n ctio n s   a n d   u s i n g   t h b asic   s y n tax   o f   J av a n d   t h m e th o d s   o f f er ed .   W d ef i n Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 A u g u s t 2 0 1 9   :   2 6 2 7   -   2636   2630   lib r ar y   cla s s e s   b ased   o n   t h f o llo w in g   c h ar ac ter is tic s   w h i ch   r ep r esen t h g e n er ic  b eh av io r   o f   n et w o r k   f u n ctio n :   -   A   n et w o r k   f u n ctio n   m a y   b eh a v as a n   e n d   h o s t o r   f o r w ar d in g   h o s t.      -   An   e n d   h o s r ep r esen t s   ter m in al  n o d e.   I ca n   r ec eiv p ac k ets,  b u t   it  ca n   al s o   s e n d   p ac k e ts   i n   r esp o n s to   r ec eiv ed   o n ( e. g .   r esp o n s to   th r eq u est)  o r   n e w   p ac k e ts   to   in itiate  co m m u n icat io n   ( e. g .   r eq u est).   E x a m p le s   o f   e n d   h o s n o d es   ar m ail  clie n t,  w eb   cl ien t,  m ail  s er v er ,   etc.   A   f o r w ar d in g   h o s t   r ep r esen t s   an   in ter m ed iate  n o d th at  p r o ce s s es  tr af f ic  ac co r d in g   to   its   in ter n al  lo g ic  to   ac co m p lis h   a   s p ec if ic  m is s io n ,   e. g .   p er f o r m i n g   N A T   tr an s la tio n ,   f ilter i n g   p ac k ets,  etc.   -   A   f o r w ar d i n g   h o s t c a n   d r o p   o r   d eter m i n w h ic h   ex it i n ter f ac to   u s to   s en d   th p ac k et  to   its   n e x t h o p .       -   A   h o s t,  ei th er   a n   e n d   o r   f o r w ar d in g   o n e,   ca n   h a v n e t w o r k   in ter f ac es   f o r   r ec eiv in g   o r   s en d i n g   p ac k et s   an d   ca n   b s ta tef u l,  i.e .   h a v e   s tate  t h at  ca n   d ep en d   o n   th h is to r y   o f   t h ac tio n s   p e r f o r m ed   b ef o r ( r elate d   to   s en t a n d   r ec eiv ed   p ac k ets).     -   T h p ac k ets  ex c h a n g ed   b y   th h o s ts   ar ab s tr ac ted   in   o r d er   to   ca p tu r o n l y   th o s c h ar ac ter is tics   t h at  ar e   r elev an f o r   v er i f icatio n .   Fo r   ex a m p le,   s o u r ce   ad d r ess ,   d est in atio n   ad d r ess ,   s o u r ce   p o r t,  d esti n atio n   p o r t,  p r o to co l u s ed ,   tar g et  UR L ,   m a il  s o u r ce ,   m ail  d es tin at io n ,   b o d y ,   etc.   C las s   d ef i n itio n :   T h d ef i n iti o n   o f   v ir tu al  n et w o r k   f u n cti o n   m u s b w r it ten   i n   u n iq u f ile  t h at   m u s e x te n d   o n o f   t h f o llo win g   t w o   ab s tr ac cla s s e s Fo r war d in g Ho s t,  E n d Ho s t   ( w h ic h   i n   t u r n   e x te n d s   t h e   Ho s class ) .   T h ese  ar th t w o   m ain   J av cla s s e s   o f   t h lib r ar y ,   w h ich   ar s u p p le m en ted   w ith   o t h er   co m p le m e n tar y   clas s es   d ep en d in g   o n   t h t y p o f   t h n et wo r k   f u n ctio n   b ein g   d escr ib ed ,   eith er   e n d   h o s o r   f o r w ar d i n g   h o s t.  Fo r   ex a m p le,   th P ac k et  clas s   d escr ib es  p ac k et  an d   o b j ec ts   o f   th is   t y p an d   t h e   R o u ti n g R e s u l class   r ep r esen ts   t h r o u tin g   d ec is io n   o f   VNF  m i g h b in clu d e d   in   E n d Ho s an d   Fo r w ar d in g Ho s t   o b j ec ts .   W h ile  th e   Ho s tT ab le  class   r ep r esen t s   a n   i n ter n al   m e m o r y   o f   t h i n ter m ed iate   n et w o r k   f u n c tio n   a n d   h en ce   is   r elate d   to   t h Fo r w ar d in g Ho s clas s   o n l y .   A d d itio n all y ,   th i n ter n alNo d es  o b j ec o f   th Ho s clas s   is   u s e d   to   d if f er en tiate  t h i n ter n al   n o d es  o f   th co r r esp o n d in g   n et w o r k   f u n c tio n   f r o m   th ex ter n al  o n e s   an d   th h o s t T ab leL is t o b j ec t sto r es th lis t o f   av ailab le  tab les.   C las s   m eth o d s :   T h b eh av io r   o f   th e   n et w o r k   f u n ctio n   m u s t   b d escr ib ed   u s in g   n u m b er   o f   p u b lic   m et h o d s   p r o v id ed   b y   th lib r a r y   cla s s es.  T h co n ten o f   th e   m et h o d s   is   u n d er   th co n tr o o f   th u s er ,   w h i c h   h as  to   s p ec i f y   t h n et w o r k   f u n ctio n   b eh a v io r   b y   m ea n s   o f   th m et h o d s   av ailab le  i n   co m p le m en tar y   cla s s es  o f   th lib r ar y .   d ef in e State( ) th i s   m et h o d   d ef in es  t h co m p o n en ts   f r o m   w h i ch   th s tate  o f   t h n et w o r k   f u n ctio n   a n d   co n f i g u r atio n   s etti n g s   ar ex tr ac t ed .   I is   p r esen eith er   if   an   E n d Ho s o r   Fo r w ar d i n g Ho s is   d ef i n ed .   T h is   m et h o d   p r o v id es  i n s tr u ct io n s   to   cr ea te  tab le  th a s to r es  p ac k et  f ield s   an d   f la g   to   i n d icate   w h eth er   th e   n et w o r k   f u n ctio n   is   ab le  to   s to r th p ac k ets r ec ei v ed   ( s en t)   o r   n o t.    d ef in e Sen d i n g P ac k e t( ) t h is   m et h o d   d ef i n es   th e   c h ar ac ter is tics   o f   t h p ac k et s   s en b y   th c u r r en t   n o d ( n o t h r e s p o n s es   to   t h r ec eiv ed   p ac k e ts   b u th e   r eq u est   p ac k et s   s e n t   b y   th e   h o s t) .   I m a y   b e   p r esen t   o n l y   if   a n   E n d Ho s i s   d ef in ed .   T h is   m e th o d   m u s r e t u r n   P a ck et  o b j ec t,  w h ich   ca n   b b u il in s id th e   m e th o d   b y   in s tan tiati n g   th P ac k et  c la s s .   T h P ac k et  class   o f f er s   m atch ( )   m et h o d   to   co m p ar th f ield s   o f   th p ac k et  ag ain s th e   o th er   f ield   o r   co n s tan ts .   T h er ar “m u tato r ”  m e th o d s   d ef i n ed   i n   t h i s   cla s s   to   c o n tr o ch a n g e s   to   a   p ac k et  f ield s .     o n R ec ei v ed P ac k et( ) th i s   m et h o d   d ef in e s   t h b eh a v io r   o f   th n et w o r k   f u n ct io n   i n   r esp o n s to   a   r ec eiv ed   p ac k et.   T h p ar am et er   o f   th o n R ec ei v ed P ac k et( )   m et h o d   is   th p ac k et  t h at  t h n et w o r k   f u n ctio n   r ec eiv es  a n d   th r etu r n   v a l u is   R o u ti n g R e s u l o b j e ct.   As  d is cu s s ed   ab o v e,   R o u tin g R es u lt  is   a   co m p le m e n tar y   cla s s   t h at  r e p r esen ts   t h r o u ti n g   d ec i s io n   o f   th VN F,  af ter   p r o ce s s i n g   o f   t h in co m i n g   p ac k et.   I ts   co n s tr u cto r   r ec eiv e s   th r ee   p ar a m eter s :   -   A   p ac k et  o b j ec t th at  t h n et w o r k   f u n ct io n   p r o d u ce s .       -   T h ac tio n   to   p er f o r m   o n   t h is   p ac k et  ( f o r w ar d   o r   d r o p ) .     -   T h f o r w ar d in g   d ir ec tio n   ( i.e .   th in ter f ac th p ac k et  is   f o r w ar d ed   to   in   ca s o f   f o r w ar d   ac tio n th is   ca n   b th u p s tr ea m   in ter f ac o r   o n o f   t h o th er   in ter f ac es o f   th n et w o r k   f u n ctio n ) .   T h ac tio n s   t h at  ca n   b in s er ted   in s id t h is   m et h o d   ar d iv id ed   in to   t h f o llo w in g   ca teg o r ies:   in s tr u ctio n s   to   ch ec k   t h co n t en ts   o f   p ac k et  f ield ,   in s tr u c tio n s   to   ch ec k   t h s tate  o f   th e   n et w o r k   f u n ctio n ,   in s tr u ctio n s   to   s to r v a lu in to   tab le   d ef in ed   b y   t h u s er ,   in s tr u ctio n s   to   d ef in th ac tio n   to   b p er f o r m ed   o n   p ac k et  ( th r o u g h   R o u ti n g R e s u lt),   an d   s etti n g   v al u i n to   f ield   o f   p ac k et.   An   e x a m p le  o f   t h J av d escr ip tio n   o f   a n   An tis p a m   n et w o r k   f u n ctio n   is   s h o w n   i n   Fi g u r 1 .   T h is   is   an   in ter m ed iar y   VNF  d esi g n e d   to   h an d le  th m ail  tr af f ic  b e t w ee n   en d   h o s ts   o n   th b asi s   o f   b lack lis tab le.   T h n a m o f   th tab le,   n u m b e r   o f   co lu m n s   ass ig n ed   f o r   t h is   tab le  an d   th t y p o f   t h tab l en tr ies  ar p ass ed   as  an   ar g u m e n to   th c o n s tr u c to r   o f   th Ho s tT ab le  class   in   th d ef i n eState( )   m et h o d   ( r o w   2 ,   Fig u r 1 ) .   I n   th i s   s ce n ar io ,   th tab le  n a m ed   B lack lis t”  co n tai n in g   s i n g le  c o lu m n   to   s to r th b lack lis ted   s en d er s   o f   e - m a il   m es s ag e s   w i th   t h t y p e n u m   Field T y p e. M A I L   FR O i s   c r ea ted .   W h er ea s   t h f o r w ar d i n g   b eh a v io r   o f   t h e   An ti s p a m   V NF  i s   d escr ib ed   u s in g   t h o n R ec ei v ed P ac k et( )   m et h o d .   I n   p ar ticu lar ,   li n es  6   an d   7   d escr ib th e   Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2 0 8 8 - 8708       A   V N F   mo d elin g   a p p r o a c h   fo r   ve r ifica tio n   p u r p o s es ( Gu id o   Ma r ch etto )   2631   f o r w ar d i n g   ac tio n   if   t h p r o to co o f   t h r ec eiv ed   p ac k et  i s   e q u al  to   P OP 3   r eq u est.  I f   th is   is   n o t h ca s e   an th p r o to co o f   th p ac k et  is   eq u al  to   P OP3   r esp o n s e,   th en   th m ail  s o u r ce   f ield   o f   t h p ac k et  m u s b ch ec k ed   a g ai n s b lac k lis en tr ies  as  s h o w n   i n   li n es  9   a n d   1 0 .   I f   th m ail  s o u r ce   f ield   o f   th P OP 3   r eq u est   p ac k et  d o es  n o m atc h   a n y   ta b le  en tr y ,   t h e n   th e   n e w   R o u ti n g R es u lt   o b j ec m u s b r et u r n ed   s p ec i f y in g   t h e   f o r w ar d i n g   ac tio n   ( lin e   1 1 ) .   Fin all y ,   l in e   1 3   co r r esp o n d s   to   d r o p   ac tio n   th a m u s b en f o r ce d   b y   t h e   n et w o r k   f u n ctio n ,   in   ca s o f   n o   o th er   co n d itio n s   ar m et.   I is   i m p o r tan to   m e n tio n   t h at   th er is   n o an y   r estrictio n   o n   th o r d er   o f   p ac k et  p r o ce s s in g   ac tio n s   p er f o r m ed   in s id th o n R ec e iv ed P ac k et( )   m et h o d ,   as  th is   is   h a n d led   ac co r d in g l y   b y   th p ar s er .           Fig u r 1 .   J av d escr ip tio n   o f   th b eh av io r   o f   th An tis p a m   n et w o r k   f u n ct io n   i n   r esp o n s to   r ec eiv ed   p ac k et       3 . 3 .   P a rser   On o f   t h m o s i m p o r tan asp ec ts   o f   o u r   ap p r o ac h   is   th p ar s er   th at  an al y s e s   th u s er   clas s   d escr ib in g   t h v ir t u al  n et w o r k   f u n ctio n .   T h p ar s er   o p er a tin g   p r in cip les  clea r l y   d ep en d   o n   th ad o p ted   v er if ica tio n   to o l.  A s   s aid   ab o v e,   th is   p ap er   co n s id er s   lo g ic - b ased   to o ls .   T h r est o f   t h is   s ec tio n   is   th e n   f o cu s ed   o n   t h is   ap p r o ac h ,   b u s i m ilar   s o lu tio n s   m i g h b ap p lied   to   d ef i n p ar s i n g   p r o ce s s es   t h at  ar s u itab le  f o r   o th er   f o r m al  v er if ica tio n   tec h n iq u es .   T h is   is   p ar o f   o u r   o n g o in g   wo r k   an d   w p la n   to   h av w id er   to o co v er ag in   n ea r   f u tu r e.     T h m ai n   f u n ctio n alitie s   o f   t h p ar s er   in   th is   f r a m e w o r k   ar th f o llo w i n g   -   th id en ti f icat io n   o f   t h i n s tr u ctio n s   i n   th J av co d th at  lea d   to   p ac k et  b ein g   s en t th r o u g h   an   i n ter f ac e   -   th id en ti f icatio n   o f   th co n d i tio n s   ( I s tate m en ts )   th at  ar tr av er s ed   to   r ea ch   th ab o v m en tio n ed   s e n d   in s tr u ctio n s .   I n   o th er   w o r d s ,   w n ee d   to   id en ti f y   all  th e   co n d itio n s   t h at   t r ig g er   a   p ac k et   s e n d in g   o p er at io n ,   w h ich   is   ac t u all y   w h a d ef i n es   th e   b eh av io r   o f   n et w o r k   f u n cti o n .   W p ar s th s o u r ce   co d to   co n v er t h ese   co n d itio n s   i n to   s p ec if ic  d ata  s tr u ctu r e,   co n s id er i n g   b o th   th f ield s   o f   t h p ac k ets  t h at  tr av er s th f u n ctio n   an d   th f u n ctio n   s tat u s ,   i f   an y .   I n   o r d er   to   d eliv er   th af o r e m e n tio n ed   f u n ctio n alitie s ,   w tak ad v an ta g o f   E clip s AST   AP I   [ 1 5 ]   in   th e x tr ac tio n   p r o ce s s   f r o m   s o u r ce   co d to   d ata  s tr u ct u r e .   I is   to o t h at  ca n   g e n er ate   an   A b s tr ac S y n tax   T r ee   ( A ST )   [ 1 6 ]   r ep r esen tatio n   o f   ex i s ti n g   J av s o u r ce   co d e.   A ST   is   r ep r esen tatio n   o f   g r ap h   in   th f o r m   o f   tr ee   f r o m   ab s tr ac t s y n tac ti s tr u ct u r o f   co d e.   Usi n g   t h i s   lib r ar y ,   o u r   p ar s er   is   ab le  to   r e p r esen t e v er y   J av f ile  a s   tr ee   o f   AST   n o d es.  T h is   s tep   h elp s   to   p er f o r m   s e m a n tic  a n al y s i s   u s i n g   th e   i n f o r m atio n   in   ea c h   n o d e,   w h er all  t h ese  n o d es  a r s p ec ialized   f o r   th s y m b o li ev en t s   o f   th J av p r o g r a m m i n g   la n g u a g e.   Fo r   ex a m p le,   th er ar n o d es  f o r   m et h o d   d ec lar atio n ,   v ar iab le   d ec lar atio n ,   ass i g n m en t,   an d   o th er s ,   w h ile  t h e   ed g es  d escr ib t h r elatio n s h i p s   b et w ee n   AST   n o d es.  I n   o t h er   w o r d s ,   th p ar s er   h elp s   to   p er f o r m   s e m a n tic   an al y s is   u s i n g   th i n f o r m atio n   in   ea c h   n o d e.   T h p ar s er   r ec u r s i v el y   v i s it s   t h A ST   o f   t h e   co d an d   s to r es  in   lo ca v ar iab les  all  t h ch ar ac t er is tics   s u c h   as:  m et h o d   d ec lar atio n s ,   v ar iab les,  co n d itio n s ,   r etu r n   p r ed icate s ,   an d   s tate m e n ts .   A l ter n ati v el y ,   th p ar s er   tak e s   s n ap s h o t”   o f   th c u r r en d e f i n itio n   o f   t h n et w o r k   f u n ct io n   an d   p r o ce ed s   in   g en er ati n g   t h f i n al  m o d el  in   ter m s   o f   h i g h - le v el  lo g ical  ex p r es s io n s .   T h f in al  m o d el  is   m o tiv a ted   b y   th v i s io n   o f   Op en   Flo w   [ 1 7 ]   f o r w ar d in g   ab s tr ac tio n   o f   t h f o r m   < m a tch ,   a ctio n > .   T h is   ab s tr ac tio n   m o d el   h a s   b ee n   b o r r o w ed   f r o m   t h e x is tin g   m o d eli n g   tec h n iq u e s   [ 1 1 ,   1 8 ]   an d   m o s o f   t h e   v er if ica tio n   to o ls   o f   f o r w ar d i n g   b eh av io r   [ 5 6 ,   1 9 ]   r ely   o n   t h m o d els ad h er in g   t h is   ab s tr ac tio n .   T o   s to r th in f o r m at io n   o b tain ed   f r o m   th n o d es,  w d ef i n ed   NFd ef i n it io n   cla s s .   I i s   s o r o f   co n ta in er ”  w h er th c h ar a cter is tics   o f   th V NF  ( e. g . ,   av ailab le  tab les,  t y p o f   th e   n et w o r k   f u n ctio n ,   p r o to co ls   u s ed   f o r   th p ac k ets   etc. )   o b tain ed   f r o m   th m et h o d s   d ef in eState( )   an d   d ef i n eS en d in g P ac k et( )   ar e   s to r ed   in   lo ca v ar iab le s .   A c co r d in g   to   th e   s tr u ctu r o f   t h o n R ec eiv ed P ac k et( )   m et h o d ,   w e   s to r i f - t h e n   s tate m en b lo ck s   i n   lis o f   I m p licatio n   o b j ec ts .   I is   b asic  f o r m   o f   i m p l icatio n   a n d   s i m p l y   s tate s   t h at   i f   s tate m en t   A   i s   tr u e,   t h e n   s ta te m e n B   i s   also   tr u e”   an d   s ep ar ated   w it h   an   i m p licatio n   ( )   s ig n .   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 A u g u s t 2 0 1 9   :   2 6 2 7   -   2636   2632   T h I m p licat io n   clas s   co n tain s   t h f o llo w i n g   s et   o f   co n d itio n   o b j ec ts   an d   is   cr ea ted   o n l y   i n   t h p r ese n ce   o f   a   f o r w ar d i n g   ac tio n :   -   ifC o n d itio n s   is   a   lis o f   co n d i tio n s   th at   ar r elate d   to   r ec eiv ed   p ac k et,   a   p ac k et  r ec ei v ed   o r   s en i n   t h e   p ast o r   an   in ter n al  s tate  o f   t h n o d e.     -   th en C o n d it io n s   i s   lis t o f   co n d itio n s   t h at  ar r elate d   to   s en d in g   p ac k et  a n d   s to r in g   i n s tr u ctio n s .     -   r esu lt   i s   co n d itio n   t h at  co n ta in s   a n   ac tio n   to   b p er f o r m ed .     I n   th n ex s tep ,   th li s o f   I m p licatio n   o b j ec ts   ar p ar titi o n ed   in to   lis o f   i m p licatio n s   b ef o r an d   af ter   th i m p licatio n   ( )   s ig n .   T h f o llo w i n g   r u les s er v as a   g u id eli n to   th i s   p ar titi o n i n g   p h ase:    -   B ef o r th i m p licatio n   s i g n ,   t h er m u s b s en d   co n d itio n   an d   all  th co n d itio n s   th at  r eg ar d   o n l y   th e   s en d i n g   p ac k e m a y   b p r esen t .   T h s en d   co n d itio n   is   co n s id er ed   at  tim t _ 0 .     -   Fo r   ev er y   p ac k et  p r ev io u s l y   s en o r   r ec eiv ed ,   a   s en d   o r   r ec eiv co n d itio n   m u s b p r esen af ter   th e   i m p licatio n   s i g n .   T h ese  co n d it io n s   ar co n s id er ed   at  ti m t _ 1   t _   -   Fo r   ev er y   s to r co n d it io n ,   a n o th er   i m p l icatio n   m u s b cr ea ted .   I h a s   t h s to r in s tr u c tio n   b e f o r th e   i m p licatio n   s i g n   a n d   all  th o t h er   co n d itio n s   a f ter   t h s i g n .   T h is   is   th w a y   in   w h ich   o u r   f r a m e w o r k   ex tr ac t s   th r eq u ir ed   in f o r m atio n   f r o m   th u s er   d ef in ed   class es  a n d   u s i n g   t h e m   cr ea te s   an   in ter n al  ab s tr ac r ep r esen tatio n   o f   th n et w o r k   f u n ct io n .   T h f u r th er   s tep ,   i.e . ,   th f i n al  cr ea tio n   o f   t h i n p u f ile  f o r   th s p ec if ic  v er if icatio n   to o l,  co n s is t s   o f   s i m p le  tr an s latio n   f r o m   th ab s tr ac m o d el  to   th s p ec if ic  in p u lan g u ag e.   O u r   f r a m e w o r k   cu r r e n tl y   i n cl u d es  tr an s lato r   f o r   th Ver iGr ap h   to o l a n d   d is cu s s ed   in   th f o llo w i n g .       4.   USE   CA SE   AN RE SUL T S   4 . 1 .   T ra ns la t io n pa t t er n.  Ver iG r a ph   ( Z 3 )   Am o n g   t h ex is ti n g   lo g ic - b as ed   v er if icatio n   to o ls ,   w s elec ted   Ver iGr ap h   [ 6 ]   as  u s ca s to   s h o h o w   th m o d el  g e n er ated   b y   th p ar s ca n   b e x p lo ited ,   af ter   p r o p e r   tr an s latio n ,   b y   r e al  v er if icatio n   to o l.  Ver iGr ap h   is   f o r m al  v er i f ica tio n   to o th at  ca n   au to m atica ll y   v er i f y   n et w o r k s   b y   c h ec k in g   ce r tain   p r o p er ties   b ef o r th r ea s er v ice  d ep lo y m e n t.  Ver iGr ap h   e x p lo its   V NF  m o d els  e x p r ess ed   as  f o r m u las  i n   f ir s o r d er   lo g ic.   T h ese  f o r m u la s   ar d if f ic u lt  to   w r ite.   He n ce ,   it  ca n   g r ea tl y   b e n ef it  f r o m   t h au to m atic  g en er atio n   o f   m o d el s .   I n   th i s   co n tex t,  th e   te r m   n e t w o r k   i s   u s ed   to   i n d icat s eq u e n ce   o f   s e v er al  n et w o r k   f u n ctio n s   ( N A T ,   w eb   ca c h e,   f ir e w al l,  I DS  a n d   s o   o n )   th at  s tar ts   f r o m   s o u r c n o d an d   en d s   in to   d i f f er e n d esti n atio n   n o d e.   I n   r esp o n s to   v er if icatio n   r eq u est,  m o d el  o f   th n et w o r k   a n d   t h i n v o lv ed   n et w o r k   f u n ct io n s ,   co n s is ti n g   o f   Fi r s Or d er   L o g ic   ( FO L )   f o r m u la s   [ 2 0 ] ,   is   c h ec k ed   ag a in s t h p r o v id ed   p o licies,  f o r   e x a m p le   r ea ch ab ilit y   p r o p er ties   b etw ee n   t w o   n o d es  in   th n et w o r k .   I n   o r d er   to   ac h iev h i g h   p er f o r m a n ce ,   t h v er if icat io n   e n g in e x p lo its   a n   o f f - t h e - s h e lf   S A T   s o lv er   ( Z 3 ) ,   w h ich   d eter m in e s   w h e th er   th co n s id er ed   p o licies  ar s atis f ied   o r   n o t,  th an k s   to   t h tr an s latio n   o f   t h es e   p r o b lem s   i n to   S A T   p r o b lem s .     Ver iGr ap h   r eq u ir es  VNF   m o d els  w r itte n   i n   a   FO L - b ased   f o r m a lis m .   He n ce ,   w e   i n clu d ed   in   o u r   f r a m e w o r k   tr an s lato r   th a tak es   ele m en ts   s to r ed   in   t h NFd ef i n itio n   o b j ec an d   c o n v er ts   th e m   in to   FO L   f o r m u las,  n a m el y ,   i n to   b o o lean   co n s tr ain t s   in   th f o r m   o f   i f - th e n   r u le - b ased   co n d itio n al  s ta te m e n t s .   Fo r   ex a m p le,   t h o n R ec eiv ed P ac k et( )   m et h o d   is   m o d eled   ac co r d in g   to   t h is   te m p late:     S END(p)  - > CONDITIONS     T h is   is   s p ec ial  la n g u a g f o r m   t h at  ca n   b in ter p r eted   th r o u g h   s atis f ac tio n   r elatio n .   I n   p ar ticu lar ,   th is   k i n d   o f   r u le  r ep r esen t s   th e   o p er atio n   o f   s en d in g   p ac k et  b y   m ea n s   o f   t h i s   r ec u r r in g   p att er n :     send( VNF, destination, packet, t0)  -   recv(source, VNF, packet, t1) && t1 < t0     S en d   a n d   r ec v   ar t w o   s p ec if ic  m et h o d s   d ef i n ed   i n   t h Ver iG r ap h   f r a m e w o r k   t h at  r ec ei v a s   an   in p u t   t w o   n o d es  r ep r esen ti n g   th e   s o u r ce   an d   t h d esti n atio n   o f   p ac k et,   p ac k et  a n d   a   ti m e.   T h ab o v f o r m u la  m ea n s   th a VNF  ca n   s e n d   p ac k et  to   g iv e n   d esti n atio n   i f   it  h as  p r ev io u s l y   r ec ei v ed   th e   p ac k et.   T h is   is   th s tar tin g   p o in t   o f   t h f i n al  r u le  th at  w i ll  b en r ic h ed   d u r i n g   th an al y s i s   d ep en d in g   o n   th e   c o n d itio n s   n ee d ed   to   f o r w ar d   th p ac k et.   T ab le  1   r ep r esen ts   t h ese  s tate m e n t s   f o r   th An ti s p a m   VN F,  as  an   ex a m p le.   I n   ess e n ce ,   it  is   t h tr a n s lat io n   o f   th e   J av a   co d d ep icted   in   Fi g u r 1 .   I f   th An ti s p a m   ( r o w   1 )   ca n   s e n d   p ac k et   p   to   t h e   n o d n 0   at  ti m t0   th en   t h p r o to co ty p o f   th p ac k et  s h o u ld   b eith er   P OP3   r e q u est  o r   r esp o n s e.   I n   ( 2 )   p ac k et  p   s h o u ld   h a v t h ad d r ess   o f   t h An tis p a m   i n   i ts   s r f ield .   I n   ( 3 )   if   th An t is p a m   ca n   s e n d   p ac k et  p   to   th n o d n 0   at  ti m e   t0   a n d   i f   th p ac k et  p r o to co t y p i s   a   P OP 3   r esp o n s e,   th en   t h es e   t wo   co n d itio n s   i m p l y   th at  t h er ex i s ts   a n o th er   n o d n 1   at  an o th er   ti m t1 ,   s u ch   th a t,  An tis p a m   r ec eiv ed   s a m p a ck et  p   f r o m   a n o th er   n o d n 1   an d   e m ail Fro m   f ield   is   n o t in   b lac k   lis t.  Fo r m u la  ( 4 )   ca n   b d escr ib ed   in   s i m ilar   w a y .   Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2 0 8 8 - 8708       A   V N F   mo d elin g   a p p r o a c h   fo r   ve r ifica tio n   p u r p o s es ( Gu id o   Ma r ch etto )   2633   T ab le  1 .   T r an s lato r   o u tp u t f o r m at  f o r   th A n t is p a m   VNF   1   s e n d ( A n t i s p a m ,   n _ 0 ,   p ,   t _ 0 )     p . p r o t o   =   =   P O P _ R EQ   p . p r o t o   =   =   P O P _ R ESP   2   se n d ( A n t i s p a m ,   n _ 0 ,   p ,   t _ 0 )     n o d e H a sA d d r ( A n t i sp a m,   p . sr c )   3   se n d ( A n t i s p a m ,   n _ 0 ,   p ,   t _ 0 )   & &   p . p r o t o ( P O P 3 _ R ESP )   →  (   n _ 1 ,   t _ 1   :     ( r e c v ( n _ 1 ,   A n t i s p a m ,   p ,   t _ 1 )   & &   t _ 1   <   t _ 0 ) )   & &   ! i s I n B l a c k L i st ( p . e mai l F r o m)   4   se n d ( A n t i s p a m ,   n _ 0 ,   p ,   t _ 0 )   & &   p . p r o t o ( P O P 3 _ R EQ )   →    (   n _ 1 ,   t _ 1   :   ( r e c v ( n _ 1 ,   A n t i s p a m ,   p ,   t _ 1 )   & &   t _ 1   <   t _ 0 ) )     5   i s I n B l a c k L i st ( p . e mai l F r o m)   =   =   f a l se   6   i f ( i s I n B l a c k L i st ( p . e mai l F r o m)   =   =   o r   ( f o r   b l   i n   l i s t   ( p . e mai l F r o m=  = b l ) )   ?   t r u e   :   f a l se       As  it  is   d o n e   f o r   ea c h   tab le  o b j ec cr ea ted   in   th J av a   co d d ef in itio n   o f   t h n et w o r k   f u n ctio n ,   t h tr an s lato r   g e n er ates  th i n ter p r etatio n   o f   t h is I n B lack L i s t( )   m et h o d   as  s h o w n   i n   f o r m u la s   ( 5 , 6 ) .   B y   d ef au l t,  th m et h o d   is   ass ig n ed   to   a   f alse  v alu e,   t h at  i s   eq u iv ale n t   to   an   e m p t y   tab le  w it h o u a n y   b lac k lis t   e n tr ies.   T h en ,   th cla u s es  in d icati n g   t h co m p ar is o n   b et w ee n   t h e m ailFro m   f ield   o f   th p ac k et  f o r   ea ch   tab le  en tr ies  in   th b lac k li s t is ad d ed   as a   d is j u n ctio n   o f   n e w   eq u alitie s   to   is I n B lack L i s t( )   in   e v er y   lo o p   iter atio n .     4 . 2 .   VNF   ca t a lo g   T h f r a m e w o r k   co m e s   w i th   s et  o f   g en er ic   VNF   m o d el s ,   w r itte n   b y   m ea n s   o f   o u r   J av lib r ar y   d u r in g   th e   d ev elo p m e n p h a s e   an d   u s ed   to   ev al u ate  t h p er f o r m a n ce   a n d   th e f f ec ti v en e s s   o f   o u r   m eth o d .   A ll   ev alu a tio n s   ar e x ec u ted   o n   a   w o r k s tat io n   w it h   8 GB   R A an d   an   I n tel  i5 - 4 2 1 0 C P a n d ,   as   d escr ib ed   in   th p r ev io u s   s ec tio n .   T h av ailab le  VNFs   ar lis ted   i n   T ab le  2 ,   to g eth er   w i th   t h p ar s in g   ti m to   g en er at e   ea ch   Ver iGr ap h   in p u m o d el.   I is   w o r th   n o tic in g   h o w   th e s t i m es  ar s atis f y in g   r esu l t,  also   co n s id er in g   t h at   th p ar s i n g   p r o ce s s   i s   n o r e al - ti m tas k   a n d   is   e x ec u ted   o n l y   o n ce   d u r in g   th e   d ata  p lan e   v er i f icatio n   p h a s e.   I n   th i s   s u b s ec tio n   w d escr ib s o m o f   t h n et w o r k   f u n ctio n s   in clu d ed   in   t h ca talo g .       T ab le  2 .   T im s p en t to   p ar s VNF  m o d els   V F N   mo d e l   T i me   t o   p a r se   ( ms)   W e b   C l i e n t   8 4 9   M a i l   C l i e n t   8 5 7   M a i l   S e r v e r   8 6 2   En d   H o st   8 6 4   I D S   8 6 9   NAT   8 8 0   W e b   S e r v e r   9 2 0   W e b   C a c h e   9 5 2   F i r e w a l l   9 5 7   A n t i sp a m   9 6 3       I DS   ( in tr u s io n   d etec tio n   s y s te m )   VNF  ac t s   s i m ilar   to   t h f ir e w all  b u I DS  p er f o r m s   ap p licatio n   la y e r   p ac k et  f ilter i n g .   I is   r ea ctiv I DS  th at  n o o n l y   d etec t s   s u s p icio u s   o r   m alicio u s   tr af f ic  an d   aler ts   th e   ad m in i s tr ato r   b u t   w ill   tak e   p r e - d ef i n ed   p r o ac tiv ac t io n s   to   r esp o n d   to   th e   t h r ea t.  T h I DS  in cl u d es  tab le  o f   t y p Field T y p e. B ODY  w ith   a   s in g le  co l u m n .   T h is   t y p o f   t h tab le  allo w s   to   s to r t h d ata  o f   L a y er   5 , 6 , 7   in   OSI   n et w o r k   m o d el.   T h I DS  in   t h is   e x a m p le,   s to r es  t h d at co r r esp o n d in g   to   th B OD Y   f ield   o f   t h p ac k e t.  I f   t h p r o to co o f   t h r ec ei v ed   p ac k et  is   eq u al   to   HT T P   R E QUE ST   o r   HT T P   R E SP ONSE   t h I DS   p er f o r m s   a   tab le  lo o k u p   b ased   o n   th B ODY  f ield   o f   th p ac k et.   T h p r esen ce   o f   an   en tr y   co r r esp o n d in g   to   th at  d ata  in   th tab le  r es u lts   i n   d r o p   ac tio n   o f   t h p ac k et.   I n   ad d itio n ,   t h is   i s   t h s tr u ctu r o f   th co d e   o f   I DS  VNF  s h ar e   in   co m m o n   w i th   An ti s p a m   V NF.   W eb   Ser v er   VNF  ch ec k s   i f   t h p r o to c o o f   th p ac k et  i s   HT T P   R E QUE ST ,   cr ea tes  n e w   p ac k et  b y   co p y i n g   all  t h f ie ld s   o f   th r ec eiv ed   p ac k et.   T h s o u r ce /d esti n atio n   I P   an d   p o r ad d r e s s es  o f   t h clo n ed   p ac k et  ar s w ap p ed   an d   P R OT OC OL   f ield   is   s et  to   HT T P   R E SP ONSE .   A n alo g o u s l y ,   Ma ilS er v er   VN d ef in i tio n   f o llo w s   t h s a m s tr u ctu r o f   t h co d e.   W eb   C ac h e   is   s tatef u VNF  co n tain i n g   tab le  o f   t w o   co lu m n s .   O n   R ec ei v ed   P ac k et   ( )   m et h o d   o f   th cla s s   co m p r is e s   f o u r   f o r w ar d in g   ac tio n s .   T h f ir s t w o   ac t io n s   co r r esp o n d   to   if   b r an c h   w h er th e   in ter f ac o f   t h ar r iv ed   p ac k et  is   in ter n al.   I f   t h P R OT OC OL   o f   th p ac k et  is   eq u a to   HT T P   R E QUE ST  an d   th tab le   co n tai n s   an   en tr y   m atch i n g   t h r eq u es ted   UR L ,   t h f o r w ar d i n g   ac tio n   is   tak e n .   T h is   f o r w ar d in g   ac tio n   is   p er f o r m ed   o n   i n ter n al  in ter f ac w it h   n e w   p ac k et  co n tai n i n g   t h r eq u es te d   w eb   p ag e.   I f   th e   r eq u ested   w eb   p ag is   n o av ailab le  in   t h tab le  o f   t h V NF,   th o r i g in al   p ac k et  i s   f o r w ar d ed   th r o u g h   th e   ex ter n al  in ter f ac e.   O n   th o t h er   h an d ,   th n e x t w o   f o r w ar d in g   ac tio n s   f o llo w   t h else  b r an ch   an d   w i th o u t   alter in g   th e   p ac k et.   Ho w e v er ,   if   t h P R OT OC O L   o f   th e   p ac k et  i s   eq u al  to   HT T P   R E SP O NSE,   w eb   co n te n t o f   th p ac k et  s to r ed   in   th tab le  o f   th V NF.    Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 A u g u s t 2 0 1 9   :   2 6 2 7   -   2636   2634   Fire w a ll   A C L   ( ac ce s s   co n tr o lis t)   en ab led   s tatele s s   n et w o r k   f u n ctio n ,   co n ta in s   tab le  o b j ec ac lT ab l e   o f   t w o   co l u m n s ,   ch ar ac ter ize d   b y   t y p Field T y p e. I P   SR C   an d   Field T y p e. I P   DE ST .   T h tab le  ac ts   as  a   b lack lis t”  a n d   if   t h p ac k et  r e ce iv ed   m atc h es t h t u p le  in   t h tab le,   d r o p   ac tio n   is   p er f o r m ed .     NA T   ( Net w o r k   A d d r ess   T r an s lato r ) -   en ab led   n et w o r k   f u n c tio n   d iv id es   th n et w o r k   in to   t w o   ar ea s   ( an   in ter n al  ar ea   an d   a n   ex ter n al  o n e)   an d   ap p lies   d if f er en r u les  o n   th i n co m in g   p ac k e ts   i f   t h e y   ar r ec eiv ed   f r o m   t h i n ter n al  o r   th e   e x ter n al  i n ter f ac e.   I n   th i s   ca s e,   p ac k ets  r ec ei v ed   f r o m   t h i n ter n a l   No d es  ar al w a y s   f o r w ar d ed   b y   r ep lacin g   t h s o u r ce   ad d r ess   f ield   o f   t h p ac k et  w it h   t h N A T   I P   ad d r ess .   W h er ea s ,   i n co m i n g   p ac k ets f r o m   th e x ter n a l in ter f ac ar f o r w ar d ed   to   th eir   d es tin atio n   o n l y   if   co n n ec tio n   al r ea d y   e x is t s .     4 . 3 .   E x peri m e nta l r esu lt s   I n   o r d er   also   to   ch ec k   th co r r ec tn es s   o f   th g e n er ated   f i n al  m o d el s ,   w co n s tr u cted   s et  o f   n et w o r k   to p o lo g ies  co n tain in g   th a v ai lab le  n et w o r k   f u n ctio n s   an d   w d e m o n s tr ate  n u m b er   o f   cu s to m   test s   o n   t h s elec ted   v er i f icatio n   to o l.  Ver iGr ap h   ca n   p er f o r m   d i f f er en k i n d s   o f   v er i f icatio n   test s r ea ch ab ilit y ,   w h ic h   co n s is ts   i n   ch ec k i n g   i f   at  leas o n p ac k et  ca n   ar r iv at  t h e   d esti n at io n   f r o m   t h s o u r ce   n o d e,   an d   is o latio n ,   w h ic h   co n s i s ts   i n   v er if y i n g   th at  n o   p ac k et  f lo w i n g   f r o m   s o u r ce   to   d esti n atio n   p ass e s   th r o u g h   ce r tain   n et w o r k   f u n ctio n .   I n   th is   s ec t io n ,   w co n s id er   r ea ch ab ilit y   p r o p er ties .   T h o v er all  n et w o r k s   b eh av io r   ( e. g . ,   ro u tin g   tab les,  m id d leb o x   co n f ig u r atio n s ,   h o s m etad ata,   etc. )   an d   th n et w o r k   to p o lo g y   i n f o r m atio n   ar r ep r esen ted   as  s e o f   ad d i tio n al  F OL   f o r m u la s   a n d   co m p leted   w it h   o th er   f o r m u la s   th at  e x p r ess   th e   p r o p er ties   to   b v er if ied   ( e. g . ,   r ea ch ab ili t y   p r o p er t y   b et w e en   t w o   n o d es   in   t h n et w o r k ) ,   in   s u c h   a   w a y   t h at  th s ati s f iab ilit y   o f   t h f o r m u l as i m p lie s   th tr u t h   o f   th s p ec if ied   p r o p er ties .     Fig u r 2   illu s tr ates  th s et  o f   to p o lo g ies  ad o p ted   f o r   o u r   test s .   Fo r   ex a m p le,   to p o lo g y   ( 1 )   in v o l v es  t w o   f ir e w alls   a n d   th r ee   en d   h o s ts .   Fire w all s   ar co n f i g u r ed   ac co r d in g   to   th f o llo w i n g   r u le s :   -   Fire w a ll 1   d en ies tr af f ic  b et w e en   h o s A   a n d   h o s C .       -   Fire w a ll 2   d en ies tr af f ic  b et w e en   h o s t B   an d   h o s t C.           Fig u r 2 .   Set o f   n et w o r k   to p o l o g ies cr ea ted   f o r   th v er i f icat i o n   p r o ce s s       T h test   in cl u d es  t w o   r ea c h ab ilit y   p r o p er ties   to   b ch ec k ed .   I n   p ar ticu lar ,   w co n s id er   t wo   p ac k ets,   o n f lo w in g   f r o m   n o d A   to   n o d C ,   an d   an o th er   f lo w i n g   f r o m   n o d A   to   n o d B .   T ak in g   i n to   ac co u n t h ab o v f ir e w all  p o licies,  w e x p ec th r ea ch ab ilit y   p r o p er ty   is   n o s a tis f ied   in   ca s o f   A - to - C ,   i n d icati n g   t h at   n o   s u c h   p ac k e ca n   e x i s t,  w h il w e x p ec it  i s   s ati s f ied   in   t h ca s o f   A - to - B .   T h o th er   t est  ca s es  ar s et  u p   as f o llo w s   ( t h n u m b er   i n   b r ac k ets r e f er s   to   th co r r esp o n d in g   to p o lo g y   in   Fi g u r 2 ) :   1.   C o n f i g u r atio n s f ir e w all  d e n ie s   tr af f ic  b et w ee n   h o s C   a n d   h o s B t h ca ch i s   s et  to   s er v an y   r eq u e s t   ( an y   U R L   o f   t h r eso u r ce   r eq u ested   i s   p r esen i n   t h ca c h e) h o s A   s en d s   an   HT T P   R E Q UE ST   to w ar d s   B h o s A   an d   C   ar s et  as  in t er n al  n o d es  o f   N A T   an d   ca ch e.   P r o p er ty r ea ch ab ilit y   b et wee n   h o s A   an d   h o s t B .   R es u lt:  n o t r ea ch ab le.   R ea s o n : c ac h n e v er   f o r w ar d s   p ac k ets to w ar d s   h o s t B .   2.   C o n f i g u r atio n s a n ti s p a m   b lo ck s   a   tr af f ic   f lo w   o r ig i n a ti n g   f r o m   ( m ail)   cl ien t,   th u s   t h er is   a   tab le  e n tr y   w it h   th ad d r ess   o f   t h ( m ai l)   clien in   th e   b l ac k li s o f   t h n et w o r k   f u n ct io n .   P r o p er t y r ea ch ab il it y   b et w ee n   m ail  s er v er   an d   ( m ai l)   clien t.  A ct io n s e n d   p ac k et  f r o m   m ail  clie n to   m ail  s e r v er .   R esu l t:  n o t   r ea ch ab le.   R ea s o n : a n ti s p a m   d r o p s   p ac k ets s en t to w ar d s   m ail   s er v er .     3.   C o n f i g u r atio n s I DS  d r o p s   p ac k et  co n tain i n g   s p ec if ic  s tr in g   i n   th b o d y   o f   t h p ac k et;  h o s s en d s   p ac k et  co n tai n i n g   t h s p ec i f i s tr in g   in   th e   b o d y .   P r o p er ty r ea ch ab il it y   b e t w ee n   h o s an d   w eb   s er v er .   R es u lt:  n o t r ea ch ab le.   R ea s o n :   I DS d r o p s   p ac k ets co n tain i n g   th s p ec if ic  s tr i n g   i n   t h b o d y   o f   th p ac k et.     4.   C o n f i g u r atio n s r eq u e s ts   ca n n o b s er v ed   b y   t h ca ch ( t h e   UR L   o f   t h r eso u r ce   r eq u este d   is   n o p r esen t   in   t h ca ch e) .   P r o p er ty r ea c h ab ilit y   b et w ee n   h o s an d   h o s B .   R es u lt r ea ch ab le.   R ea s o n :   ca ch e   f o r w ar d s   p ac k e ts ,   s i n ce   r eq u es ted   p ac k ets ar n o t p r esen t i n   ca ch tab le.     Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2 0 8 8 - 8708       A   V N F   mo d elin g   a p p r o a c h   fo r   ve r ifica tio n   p u r p o s es ( Gu id o   Ma r ch etto )   2635   5.   C o n f i g u r atio n s f ir e w all   d en i es  tr af f ic  b et w ee n   h o s a n d   w eb   s er v er ca c h is   s et  to   s er v an y   r eq u e s t.   P r o p er ty r ea ch ab ilit y   b et w ee n   h o s an d   w eb   s er v er .   R es u l t:  n o r ea ch ab le.   R ea s o n f ir e w all  b lo ck s   th e   tr af f ic  o r ig in a tin g   f r o m   h o s t a n d   ad d r ess ed   to   w eb   s er v er .   T ab le  3   d eliv er s   th r es u lts   we  o b tain ed   i m p le m e n ti n g   t h es ca teg o r ies  o f   te s ts   a n d   co n s i d er   th t w o   d if f er e n ap p r o ac h es  in   d ef i n in g   t h VN m o d els  f o r   Ver iGr ap h .   I n   p ar ticu lar ,   th tab le  in cl u d es  f ir s t   co lu m n   r e f er r ed   to   h an d co d ed   VNF  m o d el s ,   an d   s ec o n d   o n r ef er r ed   to   VNF  m o d e ls   au to g e n er ated   b y   m ea n s   o f   o u r   f r a m e w o r k .   T h s tr in g   “S A T ”  m ea n s   t h at  t h p r o p er ty   s tated   i n   t h te s t   class   is   s ati s f ied ,   w h ile  t h s tr i n g   UNS A T ”  r ef er s   to   th ca s w h er th p r o p er ty   i s   n o s atis f ied .   C o m p ar in g   th te s r es u lt s   b et w ee n   th h a n d - co d ed   m o d els  an d   t h au to m atica ll y   g en er ated   o n es  ( s tar tin g   f r o m   t h e   J av d escr ip tio n   an d   th en   g en er ated   u s i n g   t h p ar s er ) ,   w ca n   n o tice  h o w   th o b tain ed   r esu lt s   ar id en tical.   T h is   co n f ir m s   th e   co r r ec tn ess   o f   o u r   m o d elin g   a p p r o ac h   an d   also   s h o w s   t h e f f icie n c y   o f   t h d ev elo p ed   f r am e w o r k .   C o l u m n   N   r ep r esen ts   th n u m b er   o f   t h c o r r esp o n d in g   t o p o lo g y   ill u s tr a ted   in   Fig u r 2       T ab le  3 .   C o m p ar is o n   o f   th v e r i f icatio n   r es u lt s   N   T e st s   V e r i f i c a t i o n   r e su l t u si n g   h a n d - c o d e d   V N F   mo d e l   V e r i f i c a t i o n   r e su l t u si n g   a u t o g e n e r a t e d   V N F   mo d e l   T i me   t o   v e r i f y   a u t o g e n e r a t e d   V N F   mo d e l   ( ms)   ( 1 )   D o u b l e F w Te st   1   U N S A T   U N S A T   2 1 4   D o u b l e F w Te st   2   S A T   S A T   ( 2 )   C a c h e N a t F w T e st   U N S A T   U N S A T   3 1 8   ( 3 )   A n t i sp a mT e st   U N S A T   U N S A T   2 7 5   ( 4 )   I D S Te st   U N S A T   U N S A T   1 9 2   ( 5 )   C a c h e T e st   S A T   S A T   2 6 0   ( 6 )   C a c h e F w T e st   U N S A T   U N S A T   2 0 0         5.   CO NCLU SI O N   T h is   p ap er   p r esen ts   “u s er - f r ien d l y ”  ap p r o ac h   to   VNF   m o d elin g   f o r   f o r m al  v er i f icatio n   o f   VN F - b ased   n et w o r k s .   W f o cu s   o n   b r ea k in g   th b ar r ier   b etw e en   th t w o   w a y s   o f   r ep r ese n ti n g   VNF:  t h e   i m p er ativ e - ce n tr ic  f u n ctio n   d ef i n itio n   ( p r o p er   o f   VNF  d ev elo p er s )   an d   th m o r h i g h er - lev el  d ec lar ati v e   r ep r esen tatio n   ( u s ed   b y   f o r m al  v er if icatio n   e x p er ts   i n   o r d er   to   in s tr u ct  lo g ic - b ased   v er i f icatio n   to o ls ) .   T h e   p r o p o s ed   ap p r o ac h   co n s is t s   o f   tr an s lati n g   f r o m   th f o r m er   o n to   th latter   o n a u to m atica ll y .   C o n s id er in g   t h e   ea s o f   u s e,   ev e n   f o r   n o n - tech n ical  u s er s   a n d   th r eliab ilit y   i n   ter m s   o f   cr ea tio n   o f   th cla s s es th at  d escr ib t h e   b eh av io r   o f   th e   VN F,  it  i s   p o s s ib le  to   u s e   t h o u tco m o f   t h is   p r o j ec in   o th er   f u tu r e,   w i d er   w o r k s   t h at  w i ll  allo w   tr an s f o r m atio n   o f   th e   c u r r en s tr u c tu r o f   th e   n et w o r k   i n to   m o r f le x ib le,   s i m p ler   to   m a n a g a n d   ch ea p er   o n e.   C o n s id er in g   w h at  ar t h c u r r en t   r eq u est s   o f   th e   m ar k et   an d   lo o k i n g   at  t h p o s s ib le  f u t u r e   d ev elo p m en t s ,   t h is   f r a m e w o r k   p r esen ts   f u r th er   s tep   to w ar d s   th r ea i m p le m e n tatio n   o f   t h ese  n e w   co n ce p t s   in s id t h n et w o r k s .   I n   f ac t,  t h f r a m e w o r k   an d   t h a v aila b le  v er if ica tio n   to o ls   m a y   b b asic  s tr u ctu r to   d ef in Vir t u al  Net w o r k   Fu n cti o n s   an d   tes t th o v er all  n et w o r k   f u n ctio n al it y   b e f o r d ep lo y m en t.       RE F E R E NC E S   [1 ]   E.   G .   N. ,   V 1 . 1 . 1 ,   Ne t w o rk   F u n c ti o n V ir tu a li sa ti o n   (NFV);  T e r m in o lo g y ,   IEE Ne two rk ,   v o l /i ss u e :   1 ( 5 ) ,   p p .   1 - 5 0 ,   2 0 1 3 .   A v a il a b le:  h tt p :/ /i e e e x p lo re . iee e . o rg /x p ls/ab s a ll . jsp ? a rn u m b e r= 4 6 2 6 2 2 8     [2 ]   N.  P .   L o p e s,  e a l . Ch e c k in g   b e li e f in   d y n a m ic  n e t w o rk s,”   1 2 th   US ENI S y mp o si u o n   Ne two rk e d   S y ste ms   De sig n   a n d   Imp lem e n ta ti o n   ( NS DI 1 5 ) .   Oa k la n d ,   CA:  U S ENIX   Asso c ia ti o n ,   p p .   4 9 9 - 5 1 2 2 0 1 5   [3 ]   S .   Ow re ,   e a l . P v s:  A   p ro to t y p e   v e ri f ica ti o n   sy ste m ,   Pro c e e d in g o t h e   1 1 th   I n ter n a ti o n a l   Co n fer e n c e   o n   Au to m a ted   De d u c ti o n Au to ma ted   De d u c ti o n ,   se r.  CADE - 1 1 .   L o n d o n ,   UK,  UK:  S p rin g e r - Ver la g p p .   7 4 8 - 7 5 2 1 9 9 2   [4 ]   H.  M a i,   e a l . ,   De b u g g in g   th e   d a ta  p lan e   w it h   a n tea ter,”  Pro c e e d in g o t h e   ACM   S IGCO M M   2 0 1 1   C o n fer e n c e ,   se r.  S IGCO M M   ’1 1 .   Ne Y o rk ,   N Y ,   US A:   ACM p p .   2 9 0 - 3 0 1 2 0 1 1   [5 ]   R.   S to e n e sc u ,   e a l . ,   S c a lab le  S y m b o li c   E x e c u ti o n   f o M o d e rn   Ne tw o rk s,”   Pro c e e d in g o th e   A CM   S IGCO M M   2 0 1 6   C o n fer e n c e ,   p p .   3 1 4 - 3 2 7 ,   2 0 1 6 .     [6 ]   S .   S p i n o s o ,   e a l . F o rm a V e rif ica ti o n   o f   V irt u a Ne tw o rk   F u n c ti o n   G ra p h in   a n   S P - De v Op Co n tex t,   S e rv ice   Or ien ted   a n d   Cl o u d   C o mp u ti n g   -   4 th   Eu ro p e a n   Co n fer e n c e ,   ES OC 2 0 1 5 ,   T a o rm in a ,   It a ly p p .   2 5 3 - 262 2 0 1 5   [7 ]   L .   De   M o u ra   a n d   N.  Bjø rn e r,   Z 3 A n   E ff icie n S M T   S o lv e r,   Pro c e e d in g o t h e   T h e o ry   a n d   Pra c ti c e   o S o ft w a re ,   1 4 t h   In ter n a ti o n a Co n fer e n c e   o n   T o o ls  a n d   Al g o rit h ms   fo t h e   Co n str u c ti o n   a n d   A n a lys is  o S y ste ms ,   se r.   T ACA S 0 8 /E T AP S ’0 8 .   Ber li n ,   He id e lb e rg S p ri n g e r - Ver la g p p .   3 3 7 - 3 4 0 2 0 0 8 .   [8 ]   J.  C.   Co rb e t t,   e a l . Ba n d e ra ˘  Ex trac ti n g   F in it e - sta te  M o d e ls  f r o m   Ja v a   S o u rc e   Co d e ,   Pro c e e d i n g o th e   2 2 N d   In ter n a t io n a C o n fer e n c e   o n   S o ft wa re   En g in e e rin g ,   se r.  ICS E   ’0 0 .   Ne Y o rk ,   NY ,   U S A:  ACM p p .   4 3 9 - 4 4 8 2 0 0 0   [9 ]   K.  Ha v e lu n d   a n d   T .   P re ss b u rg e r,   M o d e c h e c k in g   JA V A   p ro g ra m u sin g   J A V A   P a th F in d e r,   In ter n a ti o n a l   J o u rn a o n   S o ft w a re   T o o ls f o r T e c h n o l o g y   T ra n sfe r ( S T T T ) ,   v o l / issu e :   2 ( 4 ) ,   p p .   3 6 6 - 3 8 1 ,   2 0 0 0 .     Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 A u g u s t 2 0 1 9   :   2 6 2 7   -   2636   2636   [1 0 ]   S .   K.  F a y a z ,   e a l . BUZZ:   T e stin g   Co n tex t - De p e n d e n P o li c ies   i n   S tate f u Ne t w o rk s,”   1 3 th   US E NIX  S y mp o siu m   o n   Ne tw o rk e d   S y ste ms   De sig n   a n d   Imp lem e n t a ti o n .   S a n t a   Cl a ra ,   C A:  US ENIX   Asso c ia ti o n ,   p p .   2 7 5 - 289 2 0 1 6   [1 1 ]   W .   W u ,   e a l . A u to m a ti c   s y n th e sis  o f   n f   m o d e ls  b y   p ro g ra m   a n a l y sis,”   Pro c e e d in g o t h e   1 5 t h   ACM   W o rk sh o p   o n   H o T o p ics   i n   Ne two rk s,  se r.  Ho tNets ’1 6 .   Ne Y o rk ,   NY ,   U S A ACM p p .   2 9 - 35 2 0 1 6   [1 2 ]   J.  Kh a li d ,   e a l . P a v in g   th e   w a y   f o n fv S i m p li fy in g   m id d leb o x   m o d if ica ti o n u sin g   sta tea ly z r,   Pro c e e d in g o th e   1 3 t h   Us e n ix  Co n fer e n c e   o n   Ne two rk e d   S y ste ms   D e sig n   a n d   Im p lem e n ta ti o n ,   se r.  NS DI’1 6 .   Ber k e ley ,   CA,   US A:  US ENIX   Asso c i a ti o n ,   p p .   2 3 9 - 2 5 3 2 0 1 6   [1 3 ]   M .   W e ise r,   P ro g ra m   slicin g ,   Pro c e e d in g o t h e   5 th   I n ter n a ti o n a Co n f e re n c e   o n   S o ft wa re   En g in e e rin g ,   se r.  ICS ’8 1 .   P isc a ta w a y ,   NJ ,   U S A:  IEE Pre ss p p .   4 3 9 - 4 4 9 1 9 8 1   [1 4 ]   H.  A g r a w a a n d   J.  R.   Ho rg a n ,   Dy n a m i c   p ro g ra m   slicin g ,   Pro c e e d in g o f   th e   ACM   S IGPL AN  1 9 9 0   Co n fer e n c e   o n   Pro g ra mm i n g   L a n g u a g e   De sig n   a n d   Imp lem e n t a ti o n ,   se r.  P L DI ’9 0 .   Ne Y o rk ,   US A:  ACM p p .   2 4 6 - 2 5 6 1 9 9 0   [1 5 ]   Eclip se   JD T   A P S p e c if ica ti o n ,   A v a il a b le:  h tt p :/ /h e l p . e c li p se . o rg /h e li o s/i n d e x . jsp     [1 6 ]   E.   F a u z i,   e a l . Re v e rse   e n g in e e rin g   o f   so u rc e   c o d e   to   se q u e n c e   d iag ra m   u sin g   a b stra c s y n tax   tree ,   2 0 1 6   In ter n a t io n a C o n fer e n c e   o n   D a ta   a n d   S o ft w a re   En g in e e rin g   ( ICo DS E) ,   p p .   1 - 6 ,   2 0 1 6   [1 7 ]   N.  M c Ke o w n ,   e a l . Op e n F lo w En a b li n g   In n o v a ti o n   i n   Ca m p u Ne tw o rk s,”   S IGCO M M   Co mp u t.   Co mm u n .   Rev . v ol /i ss u e :   38 ( 2 ) ,   p p .   6 9 - 7 4 ,   2 0 0 8 .     [1 8 ]   B.   T sc h a e n ,   e a l . S f c - c h e c k e r:  Ch e c k in g   th e   c o rre c f o r w a rd in g   b e h a v io o f   se rv ice   f u n c ti o n   c h a in i n g ,   NFV - S DN.  IE EE p p .   1 3 4 - 1 4 0 2 0 1 6   [1 9 ]   A .   P a n d a ,   e a l . V e rify in g   iso latio n   p ro p e rti e s in   th e   p re se n c e   o f   m id d le b o x e s ,”   Co RR ,   v o l.   a b s/ 1 4 0 9 . 7 6 8 7 ,   2 0 1 4 .     [2 0 ]   H.  B.   En d e rto n ,   A   m a th e m a ti c a in tro d u c ti o n   to   lo g ic ,   v o l /i ss u e :   40 ( 2 ) p p .   3 1 7 2 0 0 1 .       B I O G RAP H I E S   O F   AUTH O RS       G u i d o   M a r c h e tto   is  a n   a ss istan p ro f e ss o a th e   De p a rtm e n o f   Co n tr o a n d   Co m p u ter  E n g in e e rin g   o f   P o li tec n ico   d T o rin o .   He   g o h is  P h . D.  in   Co m p u ter  En g i n e e rin g   in   A p ril   2 0 0 8   f ro m   P o li tec n ic o   d T o rin o .   His  re se a rc h   to p ics   c o v e d istri b u ted   sy ste m a n d   f o r m a v e ri f ica ti o n   o f   s y ste m a n d   p ro t o c o ls.  His  in tere sts a lso   i n c lu d e   n e tw o rk   p ro t o c o ls an d   n e tw o r k   a rc h it e c tu re s.         Ric c a r d o   S isto   re c e iv e d   th e   P h . D.  d e g re e   in   Co m p u ter  En g in e e r in g   in   1 9 9 2 ,   f ro m   P o li tec n ico   d i   T o rin o ,   I taly .   S in c e   2 0 0 4 ,   h e   is F u ll   P r o f e ss o o f   Co m p u ter  En g in e e rin g   a P o li tec n ico   d T o ri n o .   Hi s   m a in   re se a r c h   in tere sts  a re   in   th e   a re a   o f   f o r m a l   m e th o d s,  a p p li e d   to   d istri b u ted   so f tw a re   a n d   c o m m u n ica ti o n   p r o to c o e n g in e e rin g ,   d istr ib u ted   sy ste m s,  a n d   c o m p u ter  se c u rit y .   He   h a a u th o re d   a n d   c o - a u th o re d   m o re   th a n   1 0 0   sc ien ti f ic p a p e rs.  He   is a S e n i o M e m b e o f   th e   A CM .         M a tte o   V irg il io   re c e iv e d   th e   M . S .   d e g re e   in   Co m p u ter  En g in e e rin g   f ro m   P o li tec n ic o   d T o rin o ,   Italy ,   in   2 0 1 2 .   He   g o t   h is   P h . D.  i n   Co n tr o a n d   C o m p u ter  E n g in e e rin g   a P o li tec n ic o   d T o rin o .   His   re se a rc h   in tere sts  in c lu d e   i n n o v a ti v e   n e tw o rk   p ro to c o ls  a n d   a rc h it e c tu re s,  C o n te n Ce n tr ic   Ne tw o rk in g   a n d   f o r m a v e rif ic a ti o n   tec h n iq u e s a p p li e d   i n   t h e   c o n tex S DN /NF V .         J a lo ll id d i n   Yu s u p o v   re c e i v e d   th e   M . S .   d e g re e   in   C o m p u ter  En g i n e e rin g   f ro m   P o li tec n ico   d i   T o rin o ,   Italy ,   in   2 0 1 6 .   Cu rre n tl y ,   He   is  a   P h . D.  st u d e n i n   C o n tr o a n d   Co m p u ter  En g in e e rin g   a P o li tec n ic o   d T o rin o .   His p rim a r y   re se a r c h   in tere sts in c lu d e   f o rm a v e ri f ica ti o n   o f   se c u rit y   p o li c ies   in   a u to m a ted   n e tw o rk   o rc h e stra ti o n .   His  o th e r   re se a r c h   in tere sts  in c lu d e   m o d e li n g ,   c y b e p h y si c a s y ste m s,  a n d   c lo u d   c o m p u ti n g   sy ste m s.     Evaluation Warning : The document was created with Spire.PDF for Python.