Safety Property: NoNetwork

property NoNetwork { 
  requires NetAddressNames, NetListenerState;

  // Don't allow any access to the network at all.

  check RNetwork.connectRemoteAddress (address: RNetAddress) {
    violation ("Attempt to access the network: opening connection "
               + address.toString ()); 
  }

  check RNetwork.preOpenListener (listener: RNetListener) {
      violation ("Attempt to access the network: opening listener "
                + listener.toString ()); 
  }

  check RNetwork.openDatagramPort (port: RNetListener) {
      violation ("Attempt to access the network: opening port "
                + port.toString ()); 
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science