Safety Property: NetConnections



property NetConnections {
    requires NetConnectionNames, NetListenerState;

    check RNetwork.connectRemoteAddress (address: RNetAddress) {
        SecurityManager security = getSecurityManager ();
    
        if (security != null) {
            security.checkConnect (address.getName (), 
                                   address.getPort ());
      
            if (address.isMulticast ()) {
                security.checkMulticast 
                    (address.getInetAddress (),
                     (byte) 1); //! should be packet ttl!
            }
        }
    }
  
    helper checkListen (port: int) {
        SecurityManager security = getSecurityManager ();
    
        if (security != null) {
            security.checkListen (port);
        }
    }

    check RNetwork.preOpenListener (listener: RNetListener) {
        checkListen (listener.getPort ());
    }
  
    check RNetwork.postOpenListener (listener: RNetListener) {
        checkListen (listener.getPort ());
    }

    check RNetwork.openDatagramPort (port: RNetListener) {
        checkListen (port.getPort ());
    }

    check RNetwork.revealHostname (name: String) {
        SecurityManager security = getSecurityManager ();
    
        if (security != null) {
            // statusMessage ("Revealing hostname: " + name);
            security.checkConnect (name, -1);
        }
    }

    check RNetwork.revealLocalHostname () {
        SecurityManager security = getSecurityManager ();
    
        if (security != null) {
            // statusMessage ("Revealing local hostname");
            security.checkConnect ("<local hostname>", -1);
        }
    }

    

    check RNetwork.postAccept (listener: RNetListener, connection: RNetConnection) {
        SecurityManager security = getSecurityManager ();
        
        if (security != null) {
            security.checkAccept (connection.getRemoteName (),
                                  connection.getRemotePort ());
        }
    }
  
    check RNetwork.joinMulticastGroup (address: RNetAddress) {
        SecurityManager security = getSecurityManager ();
    
        if (security != null) {
            security.checkMulticast (address.getInetAddress ());
        }
    }

    check RNetwork.leaveMulticastGroup (address: RNetAddress) {
        SecurityManager security = getSecurityManager ();
    
        if (security != null) {
            security.checkMulticast (address.getInetAddress ());
        }
    }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science