Safety Property: JavaAppletNetwork



property JavaAppletNetwork {
    requires NetAddressNamesNetConnectionNamesNetListenerStateNetworkBase;

    // Applets can only listen on ports >= 1024.  Port 0 is okay.
    //! check >= or >, java comments say >, code does >=!
  
    check RNetwork.preOpenListener (listener: RNetListener) {
        // debugMessage ("Open listener!");
        int port = listener.getPort ();

        if (port > 0 && port < 1024) {
            violation ("Attempt to listent to port " + port);
        }
    }

    check RNetwork.preAccept (listener: RNetListener) {
        int port = listener.getPort ();

        if (port > 0 && port < 1024) {
            violation ("Attempt to listent to port " + port);
        }
    }

    helper  checkConnect (base: String, connect: RNetConnection, trustP: boolean) {
        String fromHost;
        fromHost = base;

        if (fromHost == null) {
            return;
        }

        String toHost;
        toHost = connect.getRemoteName ();

        

        InetAddress toHostAddr, fromHostAddr;
    
        if (!fromHost.equals(toHost)) {
            try {
                // the only time we allow non-matching strings
                // is when IPs and the IPs match.
                toHostAddr = InetAddress.getByName(toHost);
                fromHostAddr = InetAddress.getByName(fromHost);
        
                if (fromHostAddr.equals(toHostAddr)) {
                    return;
                } else {
                    violation ("Illegal connection to: " + toHostAddr.toString ());
                }
            } catch (UnknownHostException e) {
                violation ("Illegal connection: " + connect.toString ());
            }  
        } else {
            try {
                toHostAddr = InetAddress.getByName (toHost);
        
                // strings match: if we have IP, we're homefree, 
                // otherwise we check the properties.
                return;
                // getBoolean really defaults to false.         
            } catch (UnknownHostException e) {
                if (trustP) {
                    return;
                } else {
                    violation ("Illegal connection (unknown host untrusted)");
                }
            }
        }
    }

    helper checkConnect (connection: RNetConnection) {
        // debugMessage ("Check connection: " + connection);

        // Applets are not allowed to open multicast connections

        if (connection.isMulticast ()) {
            violation ("Attempt to open multicast connection: " + 
                       connection.toString ());
        }
    
        checkConnect (RNetwork.getBase (), connection, 
                      Boolean.getBoolean("trustProxy"));
    }

    check RNetwork.preOpenConnection (connection: RNetConnection) {
        checkConnect (connection);
    }

    check RNetwork.postAccept (listener: RNetListener, connection: RNetConnection) {
        checkConnect (connection);
    }

    check RNetwork.joinMulticastGroup (address: RNetAddress) {
        violation ("Attempt to join multicast group.");
    }

    check RNetwork.leaveMulticastGroup (address: RNetAddress) {
        violation ("Attempt to leave multicast group.");
    }

}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science