GP-5727: Add Z3-based emulator and summarizer

This commit is contained in:
Dan
2025-06-26 18:26:42 +00:00
parent 1f1e77b780
commit 9729d240d7
81 changed files with 7705 additions and 69 deletions
+1 -1
View File
@@ -1,6 +1,6 @@
# Taint Analysis Module
This module is both a useful feature and a good reference for implementing a custom emulator
This module is both a useful feature and a good reference for implementing a custom emulator.
Users: see the help pages in Ghidra.
@@ -4,9 +4,9 @@
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
*
* http://www.apache.org/licenses/LICENSE-2.0
*
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
@@ -62,9 +62,9 @@ public class TaintSpace {
* Retrieve the taint sets for the variable at the given offset
*
* <p>
* This retrieves as many taint sets as there are elements in the given buffer vector. This
* first element becomes the taint set at the given offset, then each subsequent element becomes
* the taint set at each subsequent offset until the vector is filled. This is analogous to the
* This retrieves as many taint sets as there are elements in the given buffer vector. The first
* element becomes the taint set at the given offset, then each subsequent element becomes the
* taint set at each subsequent offset until the vector is filled. This is analogous to the
* manner in which bytes would be "read" from concrete state, starting at a given offset, into a
* destination array.
*
@@ -4,9 +4,9 @@
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
*
* http://www.apache.org/licenses/LICENSE-2.0
*
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
@@ -71,10 +71,7 @@ public class TaintTraceSpace extends TaintSpace {
* the property at the entry's offset. If the taint set is empty, we clear the property rather
* than putting the empty taint set into the property.
*
* @param map the backing object, which must now exist
* @param snap the destination snap
* @param thread if a register space, the destination thread
* @param frame if a register space, the destination frame
* @param into the trace-property access to write into
*/
public void writeDown(PcodeTracePropertyAccess<String> into) {
if (space.isUniqueSpace()) {
@@ -4,9 +4,9 @@
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
*
* http://www.apache.org/licenses/LICENSE-2.0
*
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
@@ -172,6 +172,7 @@ public class TaintPcodeEmulatorTest extends AbstractGhidraHeadlessIntegrationTes
"MOV RAX," + Syscall.CLOSE.number,
"MOV RDI,RBP",
"SYSCALL",
"MOV RAX," + Syscall.GROUP_EXIT.number,
"MOV RDI,0",