Safety Property: NoNetworkQuiet

property NoNetworkQuiet { 
  requires NetConnectionState, NetListenerState;

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

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

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

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

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science