Crypto: Adding a proof of concept bad mac ordering predicate that takes in an ArtifactNode to be used for graph generation to intercept nodes with known mac ordering issues, in order to format the node and output error messages in the graph.

bdrodes · bdrodes · commit 22c0f9fa9144 · 2025-10-20T16:24:31.000-04:00
diff --git a/java/ql/src/experimental/quantum/Examples/BadMacOrder.qll b/java/ql/src/experimental/quantum/Examples/BadMacOrder.qll
@@ -17,6 +17,13 @@ predicate isDecryptToMacFlow(ArtifactFlow::PathNode src, ArtifactFlow::PathNode
   )
 }
 
+predicate isDecryptToMacNode(Crypto::ArtifactNode node) {
+  exists(ArtifactFlow::PathNode src, ArtifactFlow::PathNode sink |
+    isDecryptToMacFlow(src, sink) and
+    node.asElement() = src.getNode().asExpr()
+  )
+}
+
 /**
  * Holds when the src node is used as plaintext input to both
  * an encryption operation and a mac operation, via the

Original file line number	Diff line number	Diff line change
`@@ -17,6 +17,13 @@ predicate isDecryptToMacFlow(ArtifactFlow::PathNode src, ArtifactFlow::PathNode`
`17`	`17`	`)`
`18`	`18`	`}`
`19`	`19`
	`20`	`+predicate isDecryptToMacNode(Crypto::ArtifactNode node) {`
	`21`	`+ exists(ArtifactFlow::PathNode src, ArtifactFlow::PathNode sink \|`
	`22`	`+ isDecryptToMacFlow(src, sink) and`
	`23`	`+ node.asElement() = src.getNode().asExpr()`
	`24`	`+ )`
	`25`	`+}`
	`26`	`+`
`20`	`27`	`/**`
`21`	`28`	`* Holds when the src node is used as plaintext input to both`
`22`	`29`	`* an encryption operation and a mac operation, via the`