Safety Property: SystemStreamChecks



property SystemStreamChecks {   
    helper securityCheckExec () {
        SecurityManager security = getSecurityManager ();
        if (security != null) { 
            security.checkExec ("setio");
        }
    }

    check RSystem.setStandardInput (st: java.io.InputStream) {
        securityCheckExec ();
    }
  
    check RSystem.setStandardOutput (st: java.io.PrintStream),
        RSystem.setStandardError (st: java.io.PrintStream) {
        securityCheckExec ();
    }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science