Safety Property: FileNetworkWall

property FileNetworkWall {
  requires NoteNetworkUse, NoteFileSystemUse, OneWallError;

  check RNetwork.preOpenConnection (connection: RNetConnection),
           RNetwork.preOpenEnd (end: RNetEnd),
           RNetwork.preOpenListener (listener: RNetListener) {
    if (RFileSystem.touched && !RNetwork.had_wall_error) {
      if (violation ("Attempt to access network after accessing files.")) {
        RNetwork.had_wall_error = true;
      }
    }
  }
  
  check RFile.RFile (pathname: String) {
    if (RNetwork.touched && !RNetwork.had_wall_error) {
      if (violation ("Attempt to access file system after accessing network.")) {
        RNetwork.had_wall_error = true;
      }
    }
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science