I nte rna t io na l J o urna l o f   E lect rica l a nd   Co m p ute r  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 l  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 F  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 t  o f   Co n tr o l  a n d   Co m p u ter E n g in e e ri n g ,   P o li tec n ico   d i  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 s  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 s  n e w  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 r  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  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 l  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 r  f o rm a l  v e ri f ica ti o n   o f   su c h   p ro p e rti e s  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 s  w rit ten   in   sp e c if ica ti o n   lan g u a g e s  th a t  a re   d if f icu lt   to   u se   f o r  p e o p le  n o t  e x p e rien c e d   in   f o rm a l  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 l  v e ri f ica ti o n   to o ls  in   re a l  sc e n a rio s,  v e n d o rs  o f   V irt u a l  Ne tw o rk   F u n c ti o n s  (V N F s)   sh o u ld   p ro v id e   a b stra c t  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 s  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 r  p re se n ts  a   f ra m e w o rk   th a t  w e   d e si g n e d   f o r  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 f  c las se s  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 l  to   tran sla te  V NF   d e f in it io n s  in t o   f o r m a l  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 t  ©   2 0 1 9   In stit u te o f  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 l  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 i  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 e  telec o m m u n ica tio n s   w o r ld   is   ex h ib it in g   a  v er y   r ap id   ch an g e  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 e  w a y   s er v ic es  ar e  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 e  co m i n g   o u t  e v er y   d a y   to   ch an g e  t h e  en t ir e  s tr u ct u r e   o f   th e  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 t  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   a  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 e  ex p ec tatio n   f o r   s i g n i f ican t  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 e  o f   th e   p r im ar y   b en e f its   o f   th e s e  s t u d i es.   T h e  v ir tu a lizat io n   tec h n o lo g y   h as  e m er g ed   a s   a  w a y   to   d ec o u p le  s o f t w ar e  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 e  an d   e n a b le  s o f t w ar e  to   r u n   i n   a  v ir t u a lized   en v ir o n m e n t,  w it h   a  co n s eq u en t  in cr ea s e  o f   th e  s er v ice   f lex ib ili t y .   I n   p ar ti cu lar ,   t h e  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 e  s tatic   n at u r e  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 t  a n d   d ep lo y m en t  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,  a  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 e  o n   t h e  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 t  r u n   o n   o n e  o r   m o r e  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 e  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 e  id ea   th at  n o w   al m o s t  an y o n e  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 e  i m p ac t  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   a  r es u lt,  a  s u b s tan t ial  a m o u n t  o f   ef f o r t  is   r eq u ir ed   to   en s u r e  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 e  p r o v ed   to   b e  p o w er f u l  e n g i n es  f o r   a  f o r m al  v er if ica tio n   o f   t h e  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 e  n e t w o r k in g   p an o r a m a,   m o s t  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   a  f o r m al  m o d el  p r o v id ed   ac co r d in g   to   a  g i v e n   d escr ip tio n   l an g u a g e.   T h e  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 e  h a v e  to   f ac e  i n   o r d er   to   en ab le   f o r m a l  v er if ica tio n   o f   v ir t u alize d   n et w o r k s   is   t h e  m o d el  co n s tr u ctio n :  t h er e  is   a  lar g e  s e m a n ti c  g ap   b et w ee n   t h e  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 e  ac ce p ted   b y   cu r r en t  v er i f icatio n   to o ls .   Fo r   ex a m p le,   p o w er f u l  ap p r o ac h es  s u c h   a s   [ 2 ]   an d   [ 5 ]   h a v e  alr ea d y   e v o l v ed   f r o m   r esear ch   a n d   ar e  n o w   b ei n g   r o lled   in to   p r o d u ctio n ,   b u t  th is   g ap   m i g h t  b e  a   s ig n i f ica n t  h u r d le  f o r   th eir   w i d e  ad o p tio n   in   r ea l  n et w o r k   e n v ir o n m en ts .   I n   ess e n ce ,   th e s e  to o ls   ar e  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   a  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 e  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 t  in p u t,  an d   u s u all y   o b lig e  d ev elo p er s   to   lear n   a  w h o le  n e w   la n g u a g e  ( e. g . ,   SE FL   i n   [ 5 ] ) .   T h is   m o ti v ate s   t h e  w o r k   p r esen ted   i n   t h is   p ap er ,   i.e . ,   a  f r a m e w o r k   f o r   a  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 e  to   p r o v id e  a  f o r m al  d escr ip tio n   o f   t h eir   f u n ctio n s   to   b e  u s ed   in   a  v er if icatio n   p r o ce s s .   T h e  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 e  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 e  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   a  w ell - k n o w n   lan g u a g e.     -   T o   leav e  s o m e  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  t h e y   c o u ld   d ef i n e  t h e  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 e  an   au to m atic  tr an s latio n   f r o m   t h e  f u n c tio n   m o d e l  d ef in itio n   in to   an   ab s tr ac t  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  t h e  ab o v e - m en tio n ed   p r in cip le s ,   w e  s elec t   J av a  as  a  w ell - k n o w n   a n d   w id e  s p r ea d   lan g u a g e  th a t  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 e  s p ec if ic  lib r ar y   w e  p r o p o s e  in   th is   J av a - b ased   f r a m e w o r k   r ep r esen ts   t h e  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 e  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   a  s k ele to n   clas s   d ef i n it io n   o f   a  g e n er ic  n et w o r k   f u n ctio n ,   a  VNF  d ev elo p er   ca n   ea s il y   e x te n d   th e  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  a  p ar s er   t h at  an al y ze s   th e   J av a  s o u r ce   co d e  an d   p r o d u ce s   an   ab s tr ac t  f o r m al  m o d el  o f   t h e  n et w o r k   f u n ctio n   t h at  ca n   b e  au to m at icall y   tr an s lated   in to   t h e  in p u t  la n g u a g e   p r o p er   o f   a  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 l  d ep en d en t  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 t  th e  v as t   m aj o r it y   o f   th e  e x is t in g   to o ls .   C u r r en tl y ,   th e  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 e  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 e  Ver iGr ap h   [ 6 ]   to o l  is   ad o p ted   as  a  u s e  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 e  h e n ce   d e v elo p ed   a  tr an s lato r   f o r   co n v er ti n g   t h e  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 e  m o d els  o b tai n e d ,   th e  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 t  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 e  t h e  d ev elo p ed   VNF  m o d el.   W e  f ir s t  in tr o d u ce   o u r   m o d eli n g   tech n iq u e  i n   Sec tio n   3 .   T h e  u s e  ca s e  an d   t h e   o b tain ed   r esu lt s   ar e  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 e  p ap er .       2.   RE L AT E D  WO RK   T h er e  h as  b ee n   a  s ig n i f ica n t  a m o u n t  o f   ac ti v it y   i n   t h e  p ast  y ea r s   o n   atte m p t in g   to   p r o v id e  a  p r o p er   s u p p o r t  f o r   th e   tr an s latio n   o f   s o f t w ar e  s y s te m   d escr ip tio n s   t o   th e  i n p u t  m o d els  f o r   v er i f ic atio n   to o ls .   Am o n g   th e  o th er s ,   w e  ca n   m e n tio n   B an d er a  [ 8 ]   an d   J av aP ath Fin d er   [ 9 ] .   T h e  t w o   ap p r o ac h es  ar e  b ased   o n   m o d el   ch ec k i n g ,   an d   th e  m o d els  th e y   e x tr ac t  ar e  m o d els  o f   J av a  s o f t w ar e.   T h e  m ai n   d if f er e n ce   w it h   r esp ec t  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 e  J av a  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 e  i n s tead   w e  d ea l  w i th   t h e  f o r w ar d i n g   b eh av io r   o f   VN Fs .   W e  ar e  n o t  in ter ested   in   all  th e  d etails  o f   th e  VNF  co d e  ex ec u tio n .   F u r th er m o r e,   w e  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 e  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   a  d o m ai n   s p ec i f ic  la n g u a g e.   A s   w e  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 e  to o ls   is   d if f ic u lt  a n d   r eq u ir es  a  d etailed   u n d er s ta n d in g   o f   th e  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 e  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   a  n et w o r k   f u n ctio n .   On   th e  o t h er   h an d ,   S y m Ne t  [ 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 e  ( SEF L ) .   W h ile   th e  w a y   t h is   la n g u a g e  h a s   b ee n   d esig n ed   h a s   s i m ilar ities   w it h   th e  J a v ab ase d   lib r ar y   w e  p r o p o s e,   th is   ap p r o ac h   lack s   t h e  id ea   o f   ea s e  o f   m o d eli n g ,   b y   in tr o d u ci n g   a  n e w   la n g u a g e.   Desp ite  th e  f ac t  t h at  t h e y   p r o v id e  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 l  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 e  w ell - k n o w n   u s er - f r ie n d l y   J av a  la n g u a g e  an d   ca n   b e  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 .   A  p r o p o s al  m o r e  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 e  s o u r ce   co d e  o f   a  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 t  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 t  r eq u ir e  a  s p ec i f ic  s tr u ct u r e  o f   t h e  s o u r ce   co d e  o f   th e  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 e  f r o m   a  g en er ali t y   p o in t  o f   v ie w .   U n f o r tu n ate l y ,   cr ea ti n g   a  m o d el  th at  ca p t u r es a ll c o d e  p ath s   o f   a  n et w o r k   f u n ctio n   i s   ch alle n g i n g ,   b ec au s e  th e  s tate  p r o ce s s in g   m a y   b e  h id d en   d ee p   in   th e  co d e.   T h is   m a y   ca u s e  t h e  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 t  u s e  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 l  w it h   t h ese   la n g u a g e  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 e  is   t h at  t h e  co d e  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 e  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 e  d ev elo p er s   th e  o p p o r tu n it y   to   i m p le m e n t  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 e  r ea l  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 e  i s   n o   s ta n d ar d   o r   m o d elin g   la n g u a g e  to   ac cu r atel y   r ep r esen t  t h e  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 t  o f   th e  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 e  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 e  v er i f icati o n   co m m u n it y .   I n   t h is   s ec tio n ,   w e  li s t  th e  o p en   p r o b lem s   t h at  w e  h a v e  e n co u n ter ed   w h i le  lo o k in g   at  t h e  p r o p o s ed   VNF  m o d els in   t h e  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 l  in   a  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 l  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  a  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 e  n ec es s it y   o f   h a v i n g   d etailed   k n o w led g e  in   t h e  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 e  t h e  b eh a v i o r   o f   a  VNF - b ased   n et w o r k ,   s t ar tin g   f r o m   a  m o r e  u s er - f r ie n d l y   d escr ip tio n   o f   th e  in v o lv ed   VNF s .   I n   p ar ticu la r ,   th e  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 e  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 e  p o w er f u l  v er if icatio n   ap p r o ac h es.    An   i m p er ati v e  la n g u a g e  s u c h   as   J av a  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  a  co d e  th at  d escr ib es  in   ex ac t  d etail  t h e   s tep s   th at  t h e  VNF  m u s t  m a k e  w h en   a  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 e  lan g u ag e s   ad o p ted   in   l o g ic - b ased   f o r m a l  v er if ica tio n   to o ls   d o   n o t sp ec if y   a  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 t  h o ld .     T h e  co n ce p tu al  g ap   b et w ee n   th e s e  t w o   r ep r ese n tatio n s   i s   th e   i m p o r tan t  c h alle n g e   s o l v ed   b y   o u r   ap p r o ac h .   T h e  p r o p o s ed   f r am e w o r k   p r o v id es  a  J a v a  lib r ar y   an d   a   p ar s er .   T h e  lib r ar y   ca n   b e  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 e  lan g u a g e.   T h e  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 e  p a r s er   tak es  as  a n   i n p u t  t h e  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 t  f o r m al  m o d el  d es cr ib in g   t h e  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 e  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 e  d ef i n itio n   t h at  is   w r itte n   i n   a  w e ll - k n o w n   lan g u ag e   in to   a  m o r e  h ig h - le v el,   d o m ai n - s p ec if ic  co n s tr ai n t  lan g u ag e ,   th at  w o u ld   b e  d if f ic u lt  to   d ea l  w it h   m a n u all y .   T h e  r est  o f   th is   s ec tio n   p r e s en t s   t h e  J av a  lib r ar y   a n d   t h e  p ar s er   w e  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 e  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 e  u s er   ca n   s i m p l y   d es cr ib e  th e  f u n ctio n a lit y   o f   th e  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 e  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 e  n et w o r k   f u n ctio n s   a n d   u s i n g   t h e  b asic   s y n tax   o f   J av a  a n d   t h e  m e th o d s   o f f er ed .   W e  d ef i n 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   2630   lib r ar y   cla s s e s   b ased   o n   t h e  f o llo w in g   c h ar ac ter is tic s   w h i ch   r ep r esen t  t h e  g e n er ic  b eh av io r   o f   a  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 e  as a n   e n d   h o s t o r   a  f o r w ar d in g   h o s t.      -   An   e n d   h o s t  r ep r esen t s   a  ter m in al  n o d e.   I t  ca n   r ec eiv e  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 e  to   a  r ec eiv ed   o n e  ( e. g .   a  r esp o n s e  to   th e  r eq u est)  o r   n e w   p ac k e ts   to   in itiate  a  co m m u n icat io n   ( e. g .   a  r eq u est).   E x a m p le s   o f   e n d   h o s t  n o d es   ar e  a  m ail  clie n t,  a  w eb   cl ien t,  a  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 e  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 e  w h ic h   ex it i n ter f ac e  to   u s e  to   s en d   th e  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   a  f o r w ar d in g   o n e,   ca n   h a v e  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 e  s ta tef u l,  i.e .   h a v e   a  s tate  t h at  ca n   d ep en d   o n   th e  h is to r y   o f   t h e  ac tio n s   p e r f o r m ed   b ef o r e  ( r elate d   to   s en t a n d   r ec eiv ed   p ac k ets).     -   T h e  p ac k ets  ex c h a n g ed   b y   th e  h o s ts   ar e  ab s tr ac ted   in   o r d er   to   ca p tu r e  o n l y   th o s e  c h ar ac ter is tics   t h at  ar e   r elev an t  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 e  d ef i n iti o n   o f   a  v ir tu al  n et w o r k   f u n cti o n   m u s t  b e  w r it ten   i n   a  u n iq u e  f ile  t h at   m u s t  e x te n d   o n e  o f   t h e  f o llo win g   t w o   ab s tr ac t  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 t  class ) .   T h ese  ar e  th e  t w o   m ain   J av a  cla s s e s   o f   t h e  lib r ar y ,   w h ich   ar e  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 e  t y p e  o f   t h e  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 t  o r   f o r w ar d i n g   h o s t.  Fo r   ex a m p le,   th e  P ac k et  clas s   d escr ib es  a  p ac k et  an d   o b j ec ts   o f   th is   t y p e  an d   t h e   R o u ti n g R e s u l t  class   r ep r esen ts   t h e  r o u tin g   d ec is io n   o f   a  VNF  m i g h t  b e  in clu d e d   in   E n d Ho s t  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 e  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 e  Fo r w ar d in g Ho s t  clas s   o n l y .   A d d itio n all y ,   th e  i n ter n alNo d es  o b j ec t  o f   th e  Ho s t  clas s   is   u s e d   to   d if f er en tiate  t h e  i n ter n al   n o d es  o f   th e  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 e  ex ter n al  o n e s   an d   th e  h o s t T ab leL is t o b j ec t sto r es th e  lis t o f   av ailab le  tab les.   C las s   m eth o d s :   T h e  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 e  d escr ib ed   u s in g   a  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 e  lib r a r y   cla s s es.  T h e  co n ten t  o f   th e   m et h o d s   is   u n d er   th e  co n tr o l  o f   th e  u s er ,   w h i c h   h as  to   s p ec i f y   t h e  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 e  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 e  lib r ar y .   d ef in e State( ) :  th i s   m et h o d   d ef in es  t h e  co m p o n en ts   f r o m   w h i ch   th e  s tate  o f   t h e  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 e  ex tr ac t ed .   I t  is   p r esen t  eith er   if   an   E n d Ho s t  o r   a  Fo r w ar d i n g Ho s t  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  a  tab le  th a t  s to r es  p ac k et  f ield s   an d   a  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 e  th e  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 e  p ac k et s   s en t  b y   th e  c u r r en t   n o d e  ( n o t  t h e  r e s p o n s es   to   t h e  r ec eiv ed   p ac k e ts   b u t  th e   r eq u est   p ac k et s   s e n t   b y   th e   h o s t) .   I t  m a y   b e   p r esen t   o n l y   if   a n   E n d Ho s t  i s   d ef in ed .   T h is   m e th o d   m u s t  r e t u r n   a  P a ck et  o b j ec t,  w h ich   ca n   b e  b u il t  in s id e  th e   m e th o d   b y   in s tan tiati n g   th e  P ac k et  c la s s .   T h e  P ac k et  class   o f f er s   a  m atch ( )   m et h o d   to   co m p ar e  th e  f ield s   o f   th e  p ac k et  ag ain s t  th e   o th er   f ield   o r   co n s tan ts .   T h er e  ar e  “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 l  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 e  b eh a v io r   o f   th e  n et w o r k   f u n ct io n   i n   r esp o n s e  to   a   r ec eiv ed   p ac k et.   T h e  p ar am et er   o f   th e  o n R ec ei v ed P ac k et( )   m et h o d   is   th e  p ac k et  t h at  t h e  n et w o r k   f u n ctio n   r ec eiv es  a n d   th e  r etu r n   v a l u e  is   a  R o u ti n g R e s u l t  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 e  r o u ti n g   d ec i s io n   o f   th e  VN F,  af ter   p r o ce s s i n g   o f   t h e  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 e  n et w o r k   f u n ct io n   p r o d u ce s .       -   T h e  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 e  f o r w ar d in g   d ir ec tio n   ( i.e .   th e  in ter f ac e  th e  p ac k et  is   f o r w ar d ed   to   in   ca s e  o f   f o r w ar d   ac tio n ;  th is   ca n   b e  th e  u p s tr ea m   in ter f ac e  o r   o n e  o f   t h e  o th er   in ter f ac es o f   th e  n et w o r k   f u n ctio n ) .   T h e  ac tio n s   t h at  ca n   b e  in s er ted   in s id e  t h is   m et h o d   ar e  d iv id ed   in to   t h e  f o llo w in g   ca teg o r ies:   in s tr u ctio n s   to   ch ec k   t h e  co n t en ts   o f   a  p ac k et  f ield ,   in s tr u c tio n s   to   ch ec k   t h e  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 e  a  v a lu e  in to   a  tab le   d ef in ed   b y   t h e  u s er ,   in s tr u ctio n s   to   d ef in e  th e  ac tio n   to   b e  p er f o r m ed   o n   a  p ac k et  ( th r o u g h   a  R o u ti n g R e s u lt),   an d   s etti n g   a  v al u e  i n to   a  f ield   o f   a  p ac k et.   An   e x a m p le  o f   t h e  J av a  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 e  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 e  m ail  tr af f ic  b e t w ee n   en d   h o s ts   o n   th e  b asi s   o f   a  b lack lis t  tab le.   T h e  n a m e  o f   th e  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 e  t y p e  o f   t h e  tab l e  en tr ies  ar e  p ass ed   as  an   ar g u m e n t  to   th e  c o n s tr u c to r   o f   th e  Ho s tT ab le  class   in   th e  d ef i n eState( )   m et h o d   ( r o w   2 ,   Fig u r e  1 ) .   I n   th i s   s ce n ar io ,   th e  tab le  n a m ed   “ B lack lis t”  co n tai n in g   a  s i n g le  c o lu m n   to   s to r e  th e  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 e  t y p e  e n u m   Field T y p e. M A I L   FR O M  i s   c r ea ted .   W h er ea s   t h e  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 e  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 e  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 e  p r o to co l  o f   t h e  r ec eiv ed   p ac k et  i s   e q u al  to   a  P OP 3   r eq u est.  I f   th is   is   n o t  t h e  ca s e   an d  th e  p r o to co l  o f   th e  p ac k et  is   eq u al  to   a  P OP3   r esp o n s e,   th en   th e  m ail  s o u r ce   f ield   o f   t h e  p ac k et  m u s t  b e  ch ec k ed   a g ai n s t  b lac k lis t  en tr ies  as  s h o w n   i n   li n es  9   a n d   1 0 .   I f   th e  m ail  s o u r ce   f ield   o f   th e  P OP 3   r eq u est   p ac k et  d o es  n o t  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 t  m u s t  b e  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   a  d r o p   ac tio n   th a t  m u s t  b e  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 e  o f   n o   o th er   co n d itio n s   ar e  m et.   I t  is   i m p o r tan t  to   m e n tio n   t h at   th er e  is   n o t  an y   r estrictio n   o n   th e  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 e  th e  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 e  p ar s er .           Fig u r e  1 .   J av a  d escr ip tio n   o f   th e  b eh av io r   o f   th e  An tis p a m   n et w o r k   f u n ct io n   i n   r esp o n s e  to   a  r ec eiv ed   p ac k et       3 . 3 .   P a rser   On e  o f   t h e  m o s t  i m p o r tan t  asp ec ts   o f   o u r   ap p r o ac h   is   th e  p ar s er   th at  an al y s e s   th e  u s er   clas s   d escr ib in g   t h e  v ir t u al  n et w o r k   f u n ctio n .   T h e  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 e  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 e  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 t  s i m ilar   s o lu tio n s   m i g h t  b e  ap p lied   to   d ef i n e  p ar s i n g   p r o ce s s es   t h at  ar e  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 t  o f   o u r   o n g o in g   wo r k   an d   w e  p la n   to   h av e  a  w id er   to o l  co v er ag e  in   a  n ea r   f u tu r e.     T h e  m ai n   f u n ctio n alitie s   o f   t h e  p ar s er   in   th is   f r a m e w o r k   ar e  th e  f o llo w i n g :    -   th e  id en ti f icat io n   o f   t h e  i n s tr u ctio n s   i n   th e  J av a  co d e  th at  lea d   to   a  p ac k et  b ein g   s en t th r o u g h   an   i n ter f ac e ;    -   th e  id en ti f icatio n   o f   th e  co n d i tio n s   ( I F  s tate m en ts )   th at  ar e  tr av er s ed   to   r ea ch   th e  ab o v e  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 e  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 t  d ef i n es   th e   b eh av io r   o f   a  n et w o r k   f u n cti o n .   W e  p ar s e  th e  s o u r ce   co d e  to   co n v er t  t h ese   co n d itio n s   i n to   a  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 e  f ield s   o f   t h e  p ac k ets  t h at  tr av er s e  th e  f u n ctio n   an d   th e  f u n ctio n   s tat u s ,   i f   an y .   I n   o r d er   to   d eliv er   th e  af o r e m e n tio n ed   f u n ctio n alitie s ,   w e  tak e  ad v an ta g e  o f   E clip s e  AST   AP I   [ 1 5 ]   in   th e  e x tr ac tio n   p r o ce s s   f r o m   s o u r ce   co d e  to   a  d ata  s tr u ct u r e .   I t  is   a  to o l  t h at  ca n   g e n er ate   an   A b s tr ac t  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 a  s o u r ce   co d e.   A ST   is   a  r ep r esen tatio n   o f   a  g r ap h   in   th e  f o r m   o f   a  tr ee   f r o m   ab s tr ac t s y n tac ti c  s tr u ct u r e  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 a  f ile  a s   a  tr ee   o f   AST   n o d es.  T h is   s tep   h elp s   to   p er f o r m   a  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 e  all  t h ese  n o d es  a r e  s p ec ialized   f o r   th e  s y m b o li c  ev en t s   o f   th e  J av a  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 e  ar e  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 e  t h e  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 e  p ar s er   h elp s   to   p er f o r m   a  s e m a n tic   an al y s is   u s i n g   th e  i n f o r m atio n   in   ea c h   n o d e.   T h e  p ar s er   r ec u r s i v el y   v i s it s   t h e  A ST   o f   t h e   co d e  an d   s to r es  in   lo ca l  v ar iab les  all  t h e  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 e  p ar s er   tak e s   a  “ s n ap s h o t”   o f   th e  c u r r en t  d e f i n itio n   o f   t h e  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 e  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 e  f in al  m o d el  is   m o tiv a ted   b y   th e  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 e  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  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 t  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 e  m o d els ad h er in g   t h is   ab s tr ac tio n .   T o   s to r e  th e  in f o r m at io n   o b tain ed   f r o m   th e  n o d es,  w e  d ef i n ed   a  NFd ef i n it io n   cla s s .   I t  i s   a  s o r t  o f   “ co n ta in er ”  w h er e  th e  c h ar a cter is tics   o f   th e  V NF  ( e. g . ,   av ailab le  tab les,  t y p e  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 e  p ac k ets   etc. )   o b tain ed   f r o m   th e  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 l  v ar iab le s .   A c co r d in g   to   th e   s tr u ctu r e  o f   t h e  o n R ec eiv ed P ac k et( )   m et h o d ,   w e   s to r e  i f - t h e n   s tate m en t  b lo ck s   i n   a  lis t  o f   I m p licatio n   o b j ec ts .   I t  is   a  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 t  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 e  I m p licat io n   clas s   co n tain s   t h e  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 e  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 t  o f   co n d i tio n s   th at   ar e  r elate d   to   a  r ec eiv ed   p ac k et,   a   p ac k et  r ec ei v ed   o r   s en t  i n   t h e   p ast o r   an   in ter n al  s tate  o f   t h e  n o d e.     -   th en C o n d it io n s   i s   a  lis t o f   co n d itio n s   t h at  ar e  r elate d   to   a  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   a  co n d itio n   t h at  co n ta in s   a n   ac tio n   to   b e  p er f o r m ed .     I n   th e  n ex t  s tep ,   th e  li s t  o f   I m p licatio n   o b j ec ts   ar e  p ar titi o n ed   in to   a  lis t  o f   i m p licatio n s   b ef o r e  an d   af ter   th e  i m p licatio n   ( ⇒ )   s ig n .   T h e  f o llo w i n g   r u les s er v e  as a   g u id eli n e  to   th i s   p ar titi o n i n g   p h ase:    -   B ef o r e  th e  i m p licatio n   s i g n ,   t h er e  m u s t  b e  a  s en d   co n d itio n   an d   all  th e  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 t  m a y   b e  p r esen t .   T h e  s en d   co n d itio n   is   co n s id er ed   at  tim e  t _ 0 .     -   Fo r   ev er y   p ac k et  p r ev io u s l y   s en t  o r   r ec eiv ed ,   a   s en d   o r   r ec eiv e  co n d itio n   m u s t  b e  p r esen t  af ter   th e   i m p licatio n   s i g n .   T h ese  co n d it io n s   ar e  co n s id er ed   at  ti m e  t _ 1   <  t _ 0    -   Fo r   ev er y   s to r e  co n d it io n ,   a n o th er   i m p l icatio n   m u s t  b e  cr ea ted .   I t  h a s   t h e  s to r e  in s tr u c tio n   b e f o r e  th e   i m p licatio n   s i g n   a n d   all  th e  o t h er   co n d itio n s   a f ter   t h e  s i g n .   T h is   is   th e  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 e  r eq u ir ed   in f o r m atio n   f r o m   th e  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 t  r ep r esen tatio n   o f   th e  n et w o r k   f u n ct io n .   T h e  f u r th er   s tep ,   i.e . ,   th e  f i n al  cr ea tio n   o f   t h e  i n p u t  f ile  f o r   th e  s p ec if ic  v er if icatio n   to o l,  co n s is t s   o f   a  s i m p le  tr an s latio n   f r o m   th e  ab s tr ac t  m o d el  to   th e  s p ec if ic  in p u t  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  a  tr an s lato r   f o r   th e  Ver iGr ap h   to o l a n d   d is cu s s ed   in   th e  f o llo w i n g .       4.   USE   CA SE   AN D  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 e  ex is ti n g   lo g ic - b as ed   v er if icatio n   to o ls ,   w e  s elec ted   Ver iGr ap h   [ 6 ]   as  a  u s e  ca s e  to   s h o w  h o w   th e  m o d el  g e n er ated   b y   th e  p ar s e  ca n   b e  e x p lo ited ,   af ter   p r o p e r   tr an s latio n ,   b y   a  r e al  v er if icatio n   to o l.  Ver iGr ap h   is   a  f o r m al  v er i f ica tio n   to o l  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 e  th e  r ea l  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 t  o r d er   lo g ic.   T h ese  f o r m u la s   ar e  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 e  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 e  a  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   a  s o u r c e  n o d e  an d   en d s   in to   a  d i f f er e n t  d esti n atio n   n o d e.   I n   r esp o n s e  to   a  v er if icatio n   r eq u est,  a  m o d el  o f   th e  n et w o r k   a n d   t h e  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 t  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  t h e  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 e  n et w o r k .   I n   o r d er   to   ac h iev e  h i g h   p er f o r m a n ce ,   t h e  v er if icat io n   e n g in e  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 e  co n s id er ed   p o licies  ar e  s atis f ied   o r   n o t,  th an k s   to   t h e  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   a  tr an s lato r   th a t  tak es   ele m en ts   s to r ed   in   t h e  NFd ef i n itio n   o b j ec t  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 e  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 e  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   a  s p ec ial  la n g u a g e  f o r m   t h at  ca n   b e  in ter p r eted   th r o u g h   a  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   a  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 e  t w o   s p ec if ic  m et h o d s   d ef i n ed   i n   t h e  Ver iG r ap h   f r a m e w o r k   t h at  r ec ei v e  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 e  d esti n atio n   o f   a  p ac k et,   a  p ac k et  a n d   a   ti m e.   T h e  ab o v e  f o r m u la  m ea n s   th a t  VNF  ca n   s e n d   a  p ac k et  to   a  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 e  s tar tin g   p o in t   o f   t h e  f i n al  r u le  th at  w i ll  b e  en r ic h ed   d u r i n g   th e  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 e  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 e  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 e  tr a n s lat io n   o f   th e   J av a   co d e  d ep icted   in   Fi g u r e  1 .   I f   th e  An ti s p a m   ( r o w   1 )   ca n   s e n d   a  p ac k et   p   to   t h e   n o d e  n 0   at  ti m e  t0   th en   t h e  p r o to co l  ty p e  o f   th e  p ac k et  s h o u ld   b e  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 e  t h e  ad d r ess   o f   t h e  An tis p a m   i n   i ts   s r c  f ield .   I n   ( 3 )   if   th e  An t is p a m   ca n   s e n d   a  p ac k et  p   to   th e  n o d e  n 0   at  ti m e   t0   a n d   i f   th e  p ac k et  p r o to co l  t y p e  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 e  ex i s ts   a n o th er   n o d e  n 1   at  an o th er   ti m e  t1 ,   s u ch   th a t,  An tis p a m   r ec eiv ed   s a m e  p a ck et  p   f r o m   a n o th er   n o d e  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 e  d escr ib ed   in   a  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 e  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 t  cr ea ted   in   th e  J av a   co d e  d ef in itio n   o f   t h e  n et w o r k   f u n ctio n ,   t h e  tr an s lato r   g e n er ates  th e  i n ter p r etatio n   o f   t h e  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 e  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 t  a n y   b lac k lis t   e n tr ies.   T h en ,   th e  cla u s es  in d icati n g   t h e  co m p ar is o n   b et w ee n   t h e  e m ailFro m   f ield   o f   th e  p ac k et  f o r   ea ch   tab le  en tr ies  in   th e  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 e  f r a m e w o r k   co m e s   w i th   a  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 a  lib r ar y   d u r in g   th e   d ev elo p m e n t  p h a s e   an d   u s ed   to   ev al u ate  t h e  p er f o r m a n ce   a n d   th e  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  e x ec u ted   o n   a   w o r k s tat io n   w it h   8 GB   R A M  an d   an   I n tel  i5 - 4 2 1 0 M  C P U  a n d ,   as   d escr ib ed   in   th e  p r ev io u s   s ec tio n .   T h e  av ailab le  VNFs   ar e  lis ted   i n   T ab le  2 ,   to g eth er   w i th   t h e  p ar s in g   ti m e  to   g en er at e   ea ch   Ver iGr ap h   in p u t  m o d el.   I t  is   w o r th   n o tic in g   h o w   th e s e  t i m es  ar e  a  s atis f y in g   r esu l t,  also   co n s id er in g   t h at   th e  p ar s i n g   p r o ce s s   i s   n o t  a  r e al - ti m e  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 e  d escr ib e  s o m e  o f   t h e  n et w o r k   f u n ctio n s   in clu d ed   in   t h e  ca talo g .       T ab le  2 .   T im e  s p en t to   p ar s e  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 e  f ir e w all  b u t  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 t  is   a  r ea ctiv e  I DS  th at  n o t  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 e  ac t io n s   to   r esp o n d   to   th e   t h r ea t.  T h e  I DS  in cl u d es  a  tab le  o f   t y p e  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 e  o f   t h e  tab le  allo w s   to   s to r e  t h e  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 e  I DS  in   t h is   e x a m p le,   s to r es  t h e  d at a  co r r esp o n d in g   to   th e  B OD Y   f ield   o f   t h e  p ac k e t.  I f   t h e  p r o to co l  o f   t h e  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 e  I DS   p er f o r m s   a   tab le  lo o k u p   b ased   o n   th e  B ODY  f ield   o f   th e  p ac k et.   T h e  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 e  tab le  r es u lts   i n   a  d r o p   ac tio n   o f   t h e  p ac k et.   I n   ad d itio n ,   t h is   i s   t h e  s tr u ctu r e  o f   th e  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 e  p r o to c o l  o f   th e  p ac k et  i s   HT T P   R E QUE ST ,   cr ea tes  a  n e w   p ac k et  b y   co p y i n g   all  t h e  f ie ld s   o f   th e  r ec eiv ed   p ac k et.   T h e  s o u r ce /d esti n atio n   I P   an d   p o r t  ad d r e s s es  o f   t h e  clo n ed   p ac k et  ar e  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 F  d ef in i tio n   f o llo w s   t h e  s a m e  s tr u ctu r e  o f   t h e  co d e.   W eb   C ac h e   is   a  s tatef u l  VNF  co n tain i n g   a  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 e  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 e  f ir s t  t w o   ac t io n s   co r r esp o n d   to   a  if   b r an c h   w h er e  th e   in ter f ac e  o f   t h e  ar r iv ed   p ac k et  is   in ter n al.   I f   t h e  P R OT OC OL   o f   th e  p ac k et  is   eq u a l  to   HT T P   R E QUE ST  an d   th e  tab le   co n tai n s   an   en tr y   m atch i n g   t h e  r eq u es ted   UR L ,   t h e  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 e  w it h   a  n e w   p ac k et  co n tai n i n g   t h e  r eq u es te d   w eb   p ag e.   I f   th e   r eq u ested   w eb   p ag e  is   n o t  av ailab le  in   t h e  tab le  o f   t h e  V NF,   th e  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 e  o t h er   h an d ,   th e  n e x t  t w o   f o r w ar d in g   ac tio n s   f o llo w   t h e  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 e  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 e  p ac k et  s to r ed   in   th e  tab le  o f   th e  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 l  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 t  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 e  Field T y p e. I P   SR C   an d   Field T y p e. I P   DE ST .   T h e  tab le  ac ts   as  a   “ b lack lis t”  a n d   if   t h e  p ac k et  r e ce iv ed   m atc h es t h e  t u p le  in   t h e  tab le,   a  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 e  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 t  r u les  o n   th e  i n co m in g   p ac k e ts   i f   t h e y   ar e  r ec eiv ed   f r o m   t h e  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 e  i n ter n a l   No d es  ar e  al w a y s   f o r w ar d ed   b y   r ep lacin g   t h e  s o u r ce   ad d r ess   f ield   o f   t h e  p ac k et  w it h   t h e  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  e x ter n a l in ter f ac e  ar e  f o r w ar d ed   to   th eir   d es tin atio n   o n l y   if   a  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 e  co r r ec tn es s   o f   th e  g e n er ated   f i n al  m o d el s ,   w e  co n s tr u cted   a  s et  o f   n et w o r k   to p o lo g ies  co n tain in g   th e  a v ai lab le  n et w o r k   f u n ctio n s   an d   w e  d e m o n s tr ate  a  n u m b er   o f   cu s to m   test s   o n   t h e  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 t  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 t  o n e  p ac k et  ca n   ar r iv e  at  t h e   d esti n at io n   f r o m   t h e  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   a  ce r tain   n et w o r k   f u n ctio n .   I n   th is   s ec t io n ,   w e  co n s id er   r ea ch ab ilit y   p r o p er ties .   T h e  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 t  m etad ata,   etc. )   an d   th e  n et w o r k   to p o lo g y   i n f o r m atio n   ar e  r ep r esen ted   as  a  s e t  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 e  v er if ied   ( e. g . ,   a  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 e  n et w o r k ) ,   in   s u c h   a   w a y   t h at  th e  s ati s f iab ilit y   o f   t h e  f o r m u l as i m p lie s   th e  tr u t h   o f   th e  s p ec if ied   p r o p er ties .     Fig u r e  2   illu s tr ates  th e  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 e  co n f i g u r ed   ac co r d in g   to   th e  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 t  A   a n d   h o s t  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 e  2 .   Set o f   n et w o r k   to p o l o g ies cr ea ted   f o r   th e  v er i f icat i o n   p r o ce s s       T h e  test   in cl u d es  t w o   r ea c h ab ilit y   p r o p er ties   to   b e  ch ec k ed .   I n   p ar ticu lar ,   w e  co n s id er   t wo   p ac k ets,   o n e  f lo w in g   f r o m   n o d e  A   to   n o d e  C ,   an d   an o th er   f lo w i n g   f r o m   n o d e  A   to   n o d e  B .   T ak in g   i n to   ac co u n t  t h e  ab o v e  f ir e w all  p o licies,  w e  e x p ec t  th e  r ea ch ab ilit y   p r o p er ty   is   n o t  s a tis f ied   in   ca s e  o f   A - to - C ,   i n d icati n g   t h at   n o   s u c h   p ac k e t  ca n   e x i s t,  w h il e  w e  e x p ec t  it  i s   s ati s f ied   in   t h e  ca s e  o f   A - to - B .   T h e  o th er   t est  ca s es  ar e  s et  u p   as f o llo w s   ( t h e  n u m b er   i n   b r ac k ets r e f er s   to   th e  co r r esp o n d in g   to p o lo g y   in   Fi g u r e  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 t  C   a n d   h o s t  B ;  t h e  ca ch e  i s   s et  to   s er v e  an y   r eq u e s t   ( an y   U R L   o f   t h e  r eso u r ce   r eq u ested   i s   p r esen t  i n   t h e  ca c h e) ;  h o s t  A   s en d s   an   HT T P   R E Q UE ST   to w ar d s   B ;  h o s t  A   an d   C   ar e  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 t  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 e  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 e  is   a   tab le  e n tr y   w it h   th e  ad d r ess   o f   t h e  ( m ai l)   clien t  in   th e   b l ac k li s t  o f   t h e  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   a  p ac k et  f r o m   m ail  clie n t  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   a  p ac k et  co n tain i n g   a  s p ec if ic  s tr in g   i n   th e  b o d y   o f   t h e  p ac k et;  h o s t  s en d s   a  p ac k et  co n tai n i n g   t h e  s p ec i f i c  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 t  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 e  s p ec if ic  s tr i n g   i n   t h e  b o d y   o f   th e  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 t  b e  s er v ed   b y   t h e  ca ch e  ( t h e   UR L   o f   t h e  r eso u r ce   r eq u este d   is   n o t  p r esen t   in   t h e  ca ch e) .   P r o p er ty :  r ea c h ab ilit y   b et w ee n   h o s t  A  an d   h o s t  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 e  n o t p r esen t i n   ca ch e  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 t  a n d   w eb   s er v er ;  ca c h e  is   s et  to   s er v e  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 t  an d   w eb   s er v er .   R es u l t:  n o t  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 e  r es u lts   we  o b tain ed   i m p le m e n ti n g   t h es e  ca teg o r ies  o f   te s ts   a n d   co n s i d er   th e  t w o   d if f er e n t  ap p r o ac h es  in   d ef i n in g   t h e  VN F  m o d els  f o r   Ver iGr ap h .   I n   p ar ticu lar ,   th e  tab le  in cl u d es  a  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   a  s ec o n d   o n e  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 e  s tr in g   “S A T ”  m ea n s   t h at  t h e  p r o p er ty   s tated   i n   t h e  te s t   class   is   s ati s f ied ,   w h ile  t h e  s tr i n g   “ UNS A T ”  r ef er s   to   th e  ca s e  w h er e  th e  p r o p er ty   i s   n o t  s atis f ied .   C o m p ar in g   th e  te s t  r es u lt s   b et w ee n   th e  h a n d - co d ed   m o d els  an d   t h e  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 a  d escr ip tio n   an d   th en   g en er ated   u s i n g   t h e  p ar s er ) ,   w e  ca n   n o tice  h o w   th e  o b tain ed   r esu lt s   ar e  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  e f f icie n c y   o f   t h e  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 e  n u m b er   o f   t h e  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 e  2       T ab le  3 .   C o m p ar is o n   o f   th e  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 s  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 s  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   a  “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 e  f o cu s   o n   b r ea k in g   th e  b ar r ier   b etw e en   th e  t w o   w a y s   o f   r ep r ese n ti n g   a  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 e  m o r e  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 e  f o r m er   o n e  to   th e  latter   o n e  a u to m atica ll y .   C o n s id er in g   t h e   ea s e  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 e  r eliab ilit y   i n   ter m s   o f   cr ea tio n   o f   th e  cla s s es th at  d escr ib e  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 e  o u tco m e  o f   t h is   p r o j ec t  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 t  s tr u c tu r e  o f   th e   n et w o r k   i n to   a  m o r e  f le x ib le,   s i m p ler   to   m a n a g e  a n d   ch ea p er   o n e.   C o n s id er in g   w h at  ar e  t h e  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 e  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   a  f u r th er   s tep   to w ar d s   th e  r ea l  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 e  t h e  n et w o r k s .   I n   f ac t,  t h e  f r a m e w o r k   an d   t h e  a v aila b le  v er if ica tio n   to o ls   m a y   b e  a  b asic  s tr u ctu r e  to   d ef in e  Vir t u al  Net w o r k   Fu n cti o n s   an d   tes t th e  o v er all  n et w o r k   f u n ctio n al it y   b e f o r e  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 s  V ir tu a li sa ti o n   (NFV);  T e r m in o lo g y , ”   IEE E  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 t  a l . ,  “ Ch e c k in g   b e li e f s  in   d y n a m ic  n e t w o rk s,”   1 2 th   US ENI X  S y mp o si u m  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 t  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 s  o f  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 t  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 s  o f  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 w  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 t  a l . ,   “ S c a lab le  S y m b o li c   E x e c u ti o n   f o r  M o d e rn   Ne tw o rk s,”   Pro c e e d in g s  o f  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 t  a l . ,  “ F o rm a l  V e rif ica ti o n   o f   V irt u a l  Ne tw o rk   F u n c ti o n   G ra p h s  in   a n   S P - De v Op s  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 C  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 t  S M T   S o lv e r, ”   Pro c e e d in g s  o f  t h e   T h e o ry   a n d   Pra c ti c e   o f  S o ft w a re ,   1 4 t h   In ter n a ti o n a l  Co n fer e n c e   o n   T o o ls  a n d   Al g o rit h ms   fo r  t h e   Co n str u c ti o n   a n d   A n a lys is  o f  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 t  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 s  o f  th e   2 2 N d   In ter n a t io n a l  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 w  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 l  c h e c k in g   JA V A   p ro g ra m s  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 l  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 t  a l . ,  “ BUZZ:   T e stin g   Co n tex t - De p e n d e n t  P o li c ies   i n   S tate f u l  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 t  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 s  o f  t h e   1 5 t h   ACM   W o rk sh o p   o n   H o t  T o p ics   i n   Ne two rk s,  se r.  Ho tNets ’1 6 .   Ne w  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 t  a l . ,  “ P a v in g   th e   w a y   f o r  n fv :  S i m p li fy in g   m id d leb o x   m o d if ica ti o n s  u sin g   sta tea ly z r, ”   Pro c e e d in g s  o f  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 s  o f  t h e   5 th   I n ter n a ti o n a l  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 E  ’8 1 .   P isc a ta w a y ,   NJ ,   U S A:  IEE E  Pre ss ,  p p .   4 3 9 - 4 4 9 ,  1 9 8 1 .    [1 4 ]   H.  A g r a w a l  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 s  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 w  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 I  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 t  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 t  s y n tax   tree , ”   2 0 1 6   In ter n a t io n a l  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 t  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 s  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 t  a l . ,  “ S f c - c h e c k e r:  Ch e c k in g   th e   c o rre c t  f o r w a rd in g   b e h a v io r  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 t  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 l  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 t  p ro f e ss o r  a t  th e   De p a rtm e n t  o f   Co n tr o l  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 i  T o rin o .   He   g o t  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 i  T o rin o .   His  re se a rc h   to p ics   c o v e r  d istri b u ted   sy ste m s  a n d   f o r m a l  v e ri f ica ti o n   o f   s y ste m s  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 r  o f   Co m p u ter  En g in e e rin g   a t  P o li tec n ico   d i  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 l  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 s  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 r  M e m b e r  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 i  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 l  a n d   C o m p u ter  E n g in e e rin g   a t  P o li tec n ic o   d i  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 t  Ce n tr ic   Ne tw o rk in g   a n d   f o r m a l  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 t  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 t  i n   C o n tr o l  a n d   Co m p u ter  En g in e e rin g   a t  P o li tec n ic o   d i  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 l  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 r  p h y si c a l  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.