MARC

 008260126s2025        us                              c    eng  d
■001000017358267
■00520260202103823
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798288862731
■035    ▼a(MiAaPQ)AAI32043035
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aDinesh,  Sushant.
■24510▼aScalable  Verification  With  Applications  to  Hardware  Security
■260    ▼a[Sl]▼bUniversity  of  California,  Berkeley▼c2025
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2025
■300    ▼a145  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  87-01,  Section:  B.
■500    ▼aAdvisor:  Fletcher,  Christopher.
■5021  ▼aThesis  (Ph.D.)--University  of  California,  Berkeley,  2025.
■520    ▼aAs  Moore's  Law  slows,  microarchitects  are  turning  to  clever  and  exotic  microarchitectural  optimizations  to  accelerate  workloads.  However,  these  optimizations  are  often  data-dependent,  inadvertently  creating  side  channels  that  leak  sensitive  information.  Disabling  them  for  security  is  impractical.  Meanwhile,  security-critical  software-such  as  cryptographic  code-lacks  visibility  into  how  its  execution  might  trigger  such  leaks.  As  these  optimizations  grow  more  complex,  writing  microarchitecturally  safe  software  will  only  become  more  difficult.  Defending  against  side-channel  attacks  therefore  demands  a  holistic,  cross-layer  approach  that  bridges  the  hardware-software  divide.This  dissertation  provides  a  methodology,  and  accompanying  formal  analyses,  to  tackle  the  microarchitectural  side  channel  problem.  Our  approach  is  two-pronged.  First,  we  verify  the  microarchitecture,  e.g.,  the  RTL,  for  security.  Once  verified,  we  obtain  software-facing  artifacts:  security-centric  microarchitectural  specifications.  Then,  we  develop  compiler-like  frameworks  that  take  leaky  code  and  derived  security  specifications  as  inputs  to  automatically  produce  microarchitecture-specific  code  that  conforms  to  the  security  specification,  guaranteeing  that  no  secrets  can  leak  through  side-channels.We  achieve  this  vision  through  three  key  technical  contributions.First,  drawing  inspiration  from  a  variety  of  side-channels  and  defenses,  we  formulate  an  instruction  set-centric  definition  to  microarchitectural  security.  We  articulate  this  as  a  formal  property:  the  Safe  Instruction  Set  Property,  SISP,  which  guarantees  that  unbounded  executions  of  a  compositions  of  instructions  do  not  leak  secrets  on  the  microarchitecture.  Verifying  if  a  set  of  instructions  satisfies  SISP  on  a  microarchitecture  gives  us  a  convenient  software-facing  abstraction:  the  set  of  instructions  that  are  safe  to  allow  compute  on  secret  data.However,  state-of-the-art  verification  tools  do  not  scale  to  verify  SISP  on  large  hardware  designs.  To  overcome  this  verification  bottleneck,  we  develop  H-Houdini,  a  new  scalable  invariant  learning  algorithm  capable  of  proving  properties  on  large  hardware  designs.  We  implement  H-Houdini  in  tool  called  VeloCT:  a  (mostly)  push-button  tool  to  verify  SISP  on  hardware  designs.  VeloCT,  for  the  first  time,  is  able  to  scale  security  verification  to  BOOM,  a  large  open-source  Out-of-Order  (OoO)  core,  in  timescales  ranging  from  6m  to  3.3h  from  the  smallest  to  the  largest  parameterization  of  BOOM.  More  importantly,  the  set  of  safe  instructions  verified  by  VeloCT  can  now  be  used  as  a  software-facing  abstraction  to  harden  code.Lastly,  we  develop  SynthCT,  a  program  synthesis  based  framework  that  uses  the  safe  set  specification  to  automatically  harden  security-critical  code  against  side-channels  on  a  specific  microarchitecture.  Notably,  SynthCT  is  a  robust,  scalable  framework  that  handles  modern,  complex  ISAs  like  x86-64  with  1000s  of  instructions,  and  is  capable  of  rewriting  even  the  most  complex  instructions,  like  division  (DIVL),  using  a  set  of  simple  safe  instructions.  We  believe  that  the  combination  of  techniques  and  tools  developed  in  this  thesis  can  serve  as  a  first  step  towards  holistic,  scalable,  automated,  principled  defenses  against  microarchitectural  side-channel  attacks.
■590    ▼aSchool  code:  0028.
■650  4▼aComputer  science
■650  4▼aEngineering
■650  4▼aInformation  technology
■653    ▼aHardware  security
■653    ▼aInvariant  learning
■653    ▼aProgram  synthesis
■653    ▼aVerification
■690    ▼a0984
■690    ▼a0489
■690    ▼a0800
■690    ▼a0537
■71020▼aUniversity  of  California,  Berkeley▼bElectrical  Engineering  &  Computer  Sciences.
■7730  ▼tDissertations  Abstracts  International▼g87-01B.
■790    ▼a0028
■791    ▼aPh.D.
■792    ▼a2025
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17358267▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

Preview

Export

ChatGPT Discussion

AI Recommended Related Books