SLAyer: Memory Safety for Systems-level Code

  • Josh Berdine ,
  • Byron Cook ,
  • Samin Ishtiaq

CAV |

SLAyer is a program analysis tool designed to automatically prove memory safety of industrial systems code. In this paper we describe SLAyer’s implementation as well as our experience applying the tool to Windows device drivers. This paper accompanies the first release of SLAyer.