MARC

 008250123s2024        us                              c    eng  d
■001000017160227
■00520250211150938
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798382193953
■035    ▼a(MiAaPQ)AAI30991449
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aAlberdingk  Thijm,  Timothy  Robin.
■24510▼aModular  Control  Plane  Verification
■260    ▼a[Sl]▼bPrinceton  University▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a186  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  85-10,  Section:  B.
■500    ▼aAdvisor:  Gupta,  Aarti.
■5021  ▼aThesis  (Ph.D.)--Princeton  University,  2024.
■520    ▼aNetworks  continue  to  experience  costly  outages  due  to  misconfigured  control  planes.  Avoiding  misconfigurations  is  challenging:  control  planes  often  use  notoriously  inscrutable  distributed  routing  protocols.  One  remedy  is  control  plane  verification,  which  analyzes  control  planes  to  uncover  violations  of  desired  properties.  Unfortunately,  most  verification  tools  analyze  the  entire  network  at  once.  Hence,  these  monolithic  tools  often  do  not  scale  well  as  networks  grow  in  size  and  properties  increase  in  complexity,  or  compromise  on  the  networks  and  properties  they  support.To  address  these  limitations,  we  explore  modular  control  plane  verification,  where  the  user  divides  their  network  into  fragments  to  verify  independently,  and  annotates  each  fragment  with  an  interface.  These  interfaces  summarize  each  fragment's  routing  announcements  (a.k.a.  routes).  We  prove  that  if  each  fragment  guarantees  its  interface,  assuming  the  interfaces  of  its  neighbors,  then  properties  of  the  fragments'  routes  hold  of  the  monolithic  network's.We  present  Kirigami,  a  formal  model  of  network  fragments  where  users  specify  interfaces  as  cuts  dividing  the  network  into  fragments,  annotating  fragment  boundaries  with  nodes'  stable  routes.  We  define  a  Satisfiability  Modulo  Theories  (SMT)-based  procedure  for  checking  interfaces,  implemented  as  an  extension  to  the  NV  (monolithic)  verification  tool.  Kirigami's  SMT  checks  are  up  to  five  orders  of  magnitude  faster  than  NV's  for  a  range  of  industrial  topologies  with  synthesized  network  policies.Unfortunately,  Kirigami's  interfaces  are  not  change-resilient  if  network  updates  change  fragments'  stable  routes.  However,  if  we  naively  extend  Kirigami's  interfaces  to  use  overapproximate  sets  of  routes  instead  of  exact  routes,  the  resulting  verification  procedure  allows  unsound  circular  reasoning.  To  prevent  circularity,  we  introduce  a  new  model,  Timepiece,  where  interfaces  are  defined  using  temporal  invariants  inspired  by  temporal  logic.  We  implement  a  new  SMT-based  checking  procedure,  which  scales  to  verify  networks  with  thousands  of  nodes  in  minutes  (compared  to  hours  for  a  monolithic  baseline)  and  allows  users  to  write  change-resilient  interfaces.
■590    ▼aSchool  code:  0181.
■650  4▼aComputer  science
■650  4▼aComputer  engineering
■650  4▼aInformation  technology
■653    ▼aAutomated  verification
■653    ▼aComputer  networks
■653    ▼aControl  planes
■653    ▼aFormal  methods
■653    ▼aModular  verification
■653    ▼aRouting
■690    ▼a0984
■690    ▼a0489
■690    ▼a0464
■71020▼aPrinceton  University▼bComputer  Science.
■7730  ▼tDissertations  Abstracts  International▼g85-10B.
■790    ▼a0181
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17160227▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

미리보기

내보내기

chatGPT토론

Ai 추천 관련 도서