property NetLimitLegalDomain (suffix: String) {
requires NetAddressNames;
check RNetwork.connectRemoteAddress (address: RNetAddress) {
if (address.getName () == null) {
NCheck.debugMessage ("No address name!");
NCheck.showStack ();
} else if (address.getName ().endsWith (suffix)) {
NCheck.debugMessage ("Address name matches: " + address.getName ());
} else {
violation
("Attempt to communicate with illegal host \"" +
address.getName () +
"\". Communication is only allowed with hosts matching suffix \"" +
suffix + "\".");
}
}
// Communication though Listeners and ends always results in a Connection,
// so no other checks are necessary.
}
Naccio Home Page
University of Virginia, Computer Science