Safety Property: JavaAppletFileSystem



property JavaAppletFileSystem {
  requires JavaAppletFileACLs, AbsoluteFileNames;

  check RFileSystem.preDelete (file: RFile) {
    // Same checking as write.
    // debugMessage ("Delete: " + file.getAbsoluteName ());

    if (!initWriteACL) {
      initWriteACLs ();
    }
    
    if (writeACL == null) {
      // debugMessage ("No write ACLs!");
      return;
    } 
    
    String realPath = file.getAbsoluteName ();

    if (!accessPermitted (writeACL, realPath)) {
      violation ("Attempt to delete file: " + realPath);
    }
  }

  // Check file observations (same as read acls)
  
  check RFileSystem.observeProperty (file: RFile), 
        RFileSystem.observeList (file: RFile) {
      if (file == null) {
          return; // this can be null during initialization!
      }

      if (!initReadACL) {
          initReadACLs ();
      }
      
      if (readACL == null) {
          // debugMessage ("No read ACLs!");
          return;
      } 
      
      String realPath = file.getAbsoluteName ();
      
      if (!accessPermitted (readACL, realPath)) {
          violation ("Attempt to observe file: " + realPath);
      }
      
      // if the applet is loaded from a file URL, allow reading
      // in that directory
      
      // NOT!
      
  }
  
  
  
  check RFileSystem.renameNew (file: RFile, newfile: RFile),
        RFileSystem.renameReplace (file: RFile, newfile: RFile) {
    if (!initWriteACL) {
      initWriteACLs ();
    }
    
    if (writeACL == null) {
      // debugMessage ("No write ACLs!");
      return;
    } 
    
    String realPath = file.getAbsoluteName ();
    
    if (!accessPermitted (writeACL, realPath)) {
      violation ("Attempt to write to file: " + realPath);
    }

    realPath = newfile.getAbsoluteName ();

    if (!accessPermitted (writeACL, realPath)) {
      violation ("Attempt to write to file: " + realPath);
    }
  }

  check RFileSystem.openOverwrite (file: RFile),
        RFileSystem.makeDirectory (file: RFile) {
      if (file == null) {
          return; // called from system code
      }

    // debugMessage ("Open write: " + file.getAbsoluteName ());
    if (!initWriteACL) {
      initWriteACLs ();
    }
    
    if (writeACL == null) {
      // debugMessage ("No write ACLs!");
      return;
    } 
    
    String realPath = file.getAbsoluteName ();
    
    if (!accessPermitted (writeACL, realPath)) {
      violation ("Attempt to write to file: " + realPath);
    }
  }

  check RFileSystem.openRead (file: RFile) {
    if (!initReadACL) {
      initReadACLs ();
    }

    if (readACL == null) {
      // debugMessage ("No read ACLs!");
      return;
    } 
    
    String realPath = file.getAbsoluteName ();
    
    if (!accessPermitted (readACL, realPath)) {
      violation ("Attempt to read file: " + realPath);
    }
    
    // if the applet is loaded from a file URL, allow reading
    // in that directory
    
    
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science