Safety Property: NetMaxTransferAmount

property NetMaxTransferAmount (maxBytes: int) {
  // Limit total data sent over the network.
  requires GlobalNetworkByteCount, OneNetTransferError;

  check RNetwork.preSend (remote: RNetAddress, nbytes: int) {
    if (!had_transfer_error) {
      if (gBytesSent + gBytesReceived + nbytes > maxBytes) {
        if (gBytesSent + gBytesReceived > 0) {
             violation 
            ("Maximum network transfer limit exceeded.  Maximum of " +
             maxBytes + " bytes. Already transferred " +
             (gBytesSent + gBytesReceived) + 
             "; attempting to send " +  nbytes + " bytes.");
        } else {
             violation 
            ("Maximum network transfer limit exceeded.  Maximum of " +
             maxBytes + " bytes; attempting to send " +  nbytes + " bytes.");
        }
      }
    }
  }

  check RNetwork.preReceive (remote: RNetAddress, nbytes: int) {
    if (!had_transfer_error) {
      if (gBytesSent + gBytesReceived + nbytes > maxBytes) {
        if (gBytesSent + gBytesReceived > 0) {
             violation 
            ("Maximum network transfer limit exceeded.  Maximum of " +
             maxBytes + " bytes. Already transferred " + 
             (gBytesSent + gBytesReceived) + 
             "; about to receive " +  nbytes + " bytes.");
        } else {
             violation 
            ("Maximum network transfer limit exceeded.  Maximum of " +
             maxBytes + " bytes; about to receive " +  nbytes + " bytes.");
        }
      }
    }
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science