Audit Specification Language

Checking Buffer Overflow:Module RequestOverflow() { msgrcv(src_mq, MSGBUF(msg), MSGSIZMAX, msgtype, flags) | (msg.type = TTRx_get) && (strlen(msg) >MSGSIZMAX) --> abort() }

Denial of Service:Spawn(“ttrx_scanner1”, &ts_mq1);Spawn(“ttrx_scanner2”, &ts_mq2)|((ttrx_scanner1 ? ttrx_scanner2) && (ts_mq1 = ts_mq2)) ->abort()

Others: (unauthorized use, listening in, etc)Spawn(“ttrx+scanner”, &ts_mq) | number-of(“ttrx_scanner”) > 7 ->abort()

Checking Buffer Overflow: Module RequestOverflow() { msgrcv(src_mq, MSGBUF(msg), MSGSIZMAX, msgtype, flags) | (msg.type = TTRx_get) && (strlen(msg) >MSGSIZMAX) --> abort() }