MARC

 008250123s2024        us                              c    eng  d
■001000017162829
■00520250211152100
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798382739588
■035    ▼a(MiAaPQ)AAI31349013
■035    ▼a(MiAaPQ)umichrackham005374
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a621.3
■1001  ▼aWintenberg,  Andrew.
■24510▼aPrivacy  and  Utility  in  Dynamic  Systems:  Verification  and  Enforcement
■260    ▼a[Sl]▼bUniversity  of  Michigan▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a155  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  85-12,  Section:  B.
■500    ▼aAdvisor:  Lafortune,  Stephane;Ozay,  Necmiye.
■5021  ▼aThesis  (Ph.D.)--University  of  Michigan,  2024.
■520    ▼aThe  development  of  cyber-physical  systems,  which  integrate  physical  processes  across  cybernetworks,  has  had  a  profound  impact  on  our  society.  Many  of  these  systems,  ranging  from  location-based  services  on  our  phones  to  devices  on  the  Internet  of  Things  in  our  homes,  rely  on  the  communication  of  sensitive  information  which  may  be  vulnerable  to  eavesdropping.  The  physical  harm  that  can  result  from  leaking  this  information,  like  your  current  location  or  the  occupancy  of  your  home,  is  well  documented.  This  has  lead  to  strict  privacy  and  security  requirements  which  are  often  difficult  to  implement  in  practice.  Motivated  by  the  success  of  formal  methods  in  developing  provable  guarantees  for  cyber-physical  systems  with  strict  safety  requirements,  in  this  dissertation  we  focus  on  the  following  problems:  (1)  How  can  we  verify  that  a  system  maintains  privacy?  and  (2)  How  can  we  enforce  privacy  upon  a  system  while  maintaining  its  original  purpose  or  utility? Verification  is  used  to  analyze  vulnerabilities  in  existing  systems  and  provide  feedback  to  guide  the  design  of  new  systems.  Existing  approaches  to  verification  are  limited  by  their  ability  to  express  complex  privacy  requirements  and  by  their  high  computational  burden.  We  propose  a  general  framework  expressing  privacy  as  the  formal  information  flow  property  of  opacity.  Over  discrete  state  models  (automata),  we  show  how  this  framework  unifies  many  of  the  existing  notions  of  opacity  studied  in  the  area  of  discrete  event  systems.  Within  this  framework,  we  develop  approaches  to  verification  based  upon  elementary  automata  constructions  that  exhibit  competitive  performance  to  existing  techniques.  Additionally,  to  overcome  the  inherent  computational  complexity  of  verification,  we  propose  a  relaxation  of  opacity  that  captures  bounds  on  the  ability  of  observers  to  reason  about  the  system.  We  develop  a  corresponding  verification  approach  based  on  an  encoding  to  the  Boolean  satisfiability  problem.  These  approaches  are  demonstrated  on  randomly  generated  systems  alongside  a  novel  server-load  hiding  problem.Enforcement  is  used  when  a  given  system  cannot  be  verified  to  maintain  privacy,  or  when  the  design  of  systems  by  hand  is  impractical.  We  focus  on  the  enforcement  of  privacy  with  obfuscation,  altering  communication  on  the  network  to  shape  the  beliefs  of  observers.  Over  systems  modeled  by  automata,  obfuscation  takes  the  form  of  edit  functions  which  dynamically  delete  certain  outputs  and  insert  fictitious  ones.  We  first  show  how  to  apply  existing  methods  for  designing  such  obfuscators  within  our  general  framework  for  opacity.  To  generalize  the  limited  notion  of  utility  guaranteed  by  these  methods,  we  then  propose  a  new  approach  to  obfuscation  which  explicitly  models  the  information  flow  from  the  system  to  its  authorized  users  as  a  distributed  system.  Finally,  we  integrate  control  into  this  approach  over  a  variety  of  network  architectures.  These  approaches  use  a  blend  of  techniques  from  supervisory  control  for  DES  and  reactive  synthesis,  and  are  demonstrated  on  a  contact-tracing  problem  as  well  as  a  smart  building  access-control  system.
■590    ▼aSchool  code:  0127.
■650  4▼aElectrical  engineering
■650  4▼aComputer  engineering
■650  4▼aInformation  technology
■653    ▼aSecurity  and  Privacy
■653    ▼aCyber-physical  systems
■653    ▼aAccess  control
■653    ▼aDiscrete  event  systems
■653    ▼aAutomata
■690    ▼a0544
■690    ▼a0489
■690    ▼a0464
■71020▼aUniversity  of  Michigan▼bElectrical  and  Computer  Engineering.
■7730  ▼tDissertations  Abstracts  International▼g85-12B.
■790    ▼a0127
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17162829▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

Preview

Export

ChatGPT Discussion

AI Recommended Related Books