Example Specifications

• utility program from untrusted source

  • open(f,m)|  (!inTree(“/tmp”, realPath(f)) && writeMode(m))|| (!accessible(realPath(f),m,”nobody”)))--> fake(EACCES)

• FTP Server

  • execve(“in.ftpd”);(!setreuid())*;  (open(f)| f ? ftpAdminFiles) --> fake(EACCES)

• race conditions on file access

  • nonatomic(f.target) in  [permCheck(f); (!(permCheck|writeOpen(f))*);writeOpen(f)] --> fake(EACCES)

Previous slide

Next slide

Back to first slide

View graphic version