property LimitBytesRead (limit: int) {
requires TrackTotalBytesRead, OneReadError, FileNames;
check RFileSystem.postRead (file: RFile, n: int) {
// We use had_read_error (defined by OneReadError) to
// only report a violation for the first read error
// encountered. This is useful for testing, but wouldn't
// be a safe thing to do in a deployed policy.
if (!had_read_error) {
if (bytes_read + n > limit) {
if (bytes_read > 0) {
if (file == null) {
violation
("Attempt to read more than " + limit +
" bytes. Already read " + bytes_read +
" bytes, reading " + n + " more.");
} else {
violation
("Attempt to read more than " + limit +
" bytes. Already read " + bytes_read +
" bytes, reading " + n + " more from " +
file.getName () + ".");
}
} else {
if (file == null) {
violation
("Attempt to read more than " + limit +
" bytes. Reading " + n + ".");
} else {
violation
("Attempt to read more than " + limit +
" bytes. Reading " + n + " from " +
file.getName () + ".");
}
}
}
}
}
}
Naccio Home Page
University of Virginia, Computer Science