Safety Property: JavaAppletThreads

property JavaAppletThreads {
  requires TrackThreadsTrackThreadGroups

  // Applets are not allowed to manipulate threads outside applet
  // thread group, but may manipulate applet threads.
  // (err...unfortunately, there is no way to determine which is which.)

  // moved to TrackThreads
  // helper RSystemThreads.inThreadGroup (g: RThreadGroup) returns boolean {
    // This is a kludge, copies from AppletSecurity.java

    

  // return false;
  // }

  helper RSystemThreads.checkThreadAccess (thread: RThread) {
    // AppletSecurity checks classLoadDepth() == 3 && ...?
    // Doesn't make sense to me...

    if (!thread.inThreadGroup (thread.getThreadGroup ())) {
      violation ("Illegal thread access: " + thread.toString ());
    }
  }
  
  check RSystemThreads.setThreadName (thread: RThread, name: String) {
    checkThreadAccess (thread);
  }

  check RSystemThreads.setDaemonThread (thread: RThread),
           RSystemThreads.setUserThread (thread: RThread) {
    checkThreadAccess (thread);
  }     
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science