chore: refractor, add tests

.github/workflows/test.yml

@@ -20,7 +20,7 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - name: Setup Python
-        uses: actions/setup-python@v4.5.0
+        uses: actions/setup-python@v4
         with:
           python-version: '3.7'
           cache: pip
@@ -30,7 +30,7 @@ jobs:
         run: pip install -r requirements.txt
       - name: Cache wabt
         id: cache-wabt
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         with:
           path: wabt-1.0.32
           key: wabt

SymGX.py

@@ -1,15 +1,7 @@
 #!/usr/bin/env python3
 # -*- coding: utf-8 -*-
 
-import argparse
-import json
 import os
-import sys
-from datetime import datetime
-
-from eunomia.arch.wasm.configuration import Configuration
-from eunomia.arch.wasm.pathgraph import Graph
-from eunomia.arch.wasm.visualizator import visualize
 from eunomia.arch.wasm.mythread import multi_thread_process
 
 def SymGX(args):
@@ -44,7 +36,4 @@ def SymGX(args):
         max_time = args.max_time
     print("set time limit: %d seconds" % max_time)
 
-    # import necessary part
-    from eunomia.arch.wasm.emulator import WasmSSAEmulatorEngine
-
     multi_thread_process(octo_bytecode, namelist, Ecall_list, max_time)

eunomia/arch/wasm/mythread.py

@@ -33,8 +33,9 @@ def Init_state(wasmVM, func):
     return wasmVM.init_state(func, param_str)
 
 class myThread(Thread):
-    def __init__(self):
+    def __init__(self, results):
         Thread.__init__(self)
+        self.results = results
 
     def run(self):
         from eunomia.arch.wasm.pathgraph import Graph
@@ -65,6 +66,8 @@ def run(self):
             else:
                 state_pool_lock.release()
                 print('Thread id : %d gets nothing, now exits.' % t.ident)
+                break
+        self.results.append(0)
 
 def multi_thread_process(octocode, namelist, Ecall_list, max_time):
     global GlobalEcallList
@@ -85,8 +88,9 @@ def multi_thread_process(octocode, namelist, Ecall_list, max_time):
     global alive
     alive = True
     threadlist = []
+    results = []
     for i in range(CoreNum):
-        threadlist.append(myThread())
+        threadlist.append(myThread(results))
 
     for thread in threadlist:
         thread.start()
@@ -101,3 +105,7 @@ def multi_thread_process(octocode, namelist, Ecall_list, max_time):
 
     for thread in threadlist:
         thread.join()
+
+    assert len(results) == CoreNum, "Some threads did not exit properly"
+    for result in results:
+        assert result == 0

main.py

@@ -8,14 +8,74 @@
 from os import makedirs, path
 
 import sh
-from launch import launch
-from SymGX import SymGX
 
+from seewasm.arch.wasm.configuration import Configuration
 
+def do_symgx(args):
+    from SymGX import SymGX
+    # ecall_list must be specified
+    if not args.ecall_list:
+        print("Error: --symgx requires --ecall-list")
+        exit(1)
+    SymGX(args)
 
-def main():
+def do_normal(args):
+    module_bytecode = args.file.read()
+    # create the corresponding wat file
+    wat_file_path = args.file.name.replace('.wasm', '.wat')
+    if not path.exists(wat_file_path):
+        sh.Command('wasm2wat')([args.file.name, "-o", wat_file_path])
+        print(
+            f"The corresponding wat file is written in: {wat_file_path}",
+            flush=True)
+    # conduct symbolic execution
+    if args.symbolic:
+        Configuration.set_verbose_flag(args.verbose)
+        Configuration.set_entry(args.entry)
+        Configuration.set_visualize(args.visualize)
+        Configuration.set_source_type(args.source_type)
+        Configuration.set_stdin(args.stdin, args.sym_stdin)
+        Configuration.set_sym_files(args.sym_files)
+        Configuration.set_incremental_solving(args.incremental)
+        Configuration.set_elem_index_to_func(wat_file_path)
+
+        command_file_name = f"./log/result/{Configuration.get_file_name()}_{Configuration.get_start_time()}/command.json"
+        makedirs(path.dirname(command_file_name), exist_ok=True)
+        with open(command_file_name, 'w') as fp:
+            json.dump({"Command": " ".join(sys.argv)}, fp, indent=4)
+
+        # --args and --sym_args can exist simultaneously
+        # their order are fixed, i.e., --args is in front of --sym_args
+        # the file_name is always the argv[0]
+        Configuration.set_args(
+            Configuration.get_file_name(),
+            args.args, args.sym_args)
+
+        # import necessary part
+        from seewasm.arch.wasm.emulator import WasmSSAEmulatorEngine
+        from seewasm.arch.wasm.graph import Graph
+        from seewasm.arch.wasm.visualizator import visualize
+
+        wasmVM = WasmSSAEmulatorEngine(module_bytecode)
+        # run the emulator for SSA
+        Graph.wasmVM = wasmVM
+        Graph.initialize()
+        # draw the ICFG on basic block level, and exit
+        if Configuration.get_visualize():
+            # draw here
+            visualize(Graph)
+
+            print(f"The visualization of ICFG is done.")
+            return
+
+        graph = Graph()
+        graph.traverse()
+    else:
+        pass
+
+def parse():
     parser = argparse.ArgumentParser(
-        description='SeeWasm, a symbolic execution engine for Wasm module')
+        description='WASEM, a general symbolic execution framework for WebAssembly (WASM) binaries ')
 
     inputs = parser.add_argument_group('Input arguments')
     inputs.add_argument('-f', '--file',
@@ -75,28 +135,28 @@ def main():
     symgx.add_argument('--func-list', help='function list string, separated by commas (`,`)')
 
     args = parser.parse_args()
+    return args
 
-    if args.symgx:
-        # ecall_list must be specified
-        if not args.ecall_list:
-            parser.error("--symgx requires --ecall-list")
-            exit(1)
-        SymGX(args)
-    else:
-        launch(args)
-
-if __name__ == '__main__':
+def main():
+    args = parse()
     job_start_time = datetime.now()
     current_time_start = job_start_time.strftime("%Y-%m-%d %H:%M:%S")
     print(f"Start to analyze: {current_time_start}", flush=True)
-    #Configuration.set_start_time(current_time_start)
-
+    Configuration.set_file(args.file.name)
+    Configuration.set_start_time(job_start_time.strftime("%Y%m%d%H%M%S"))
     print(f"Running...", flush=True)
-    main()
-    print(f"Finished.", flush=True)
 
+    if args.symgx:
+        do_symgx(args)
+    else:
+        do_normal(args)
+
+    print(f"Finished.", flush=True)
     job_end_time = datetime.now()
     current_time_end = job_end_time.strftime("%Y-%m-%d %H:%M:%S")
     print(f"End of analyze: {current_time_end}", flush=True)
     elapsed_time = job_end_time - job_start_time
     print(f"Time elapsed: {elapsed_time}", flush=True)
+
+if __name__ == '__main__':
+    main()

test/test.py

@@ -1,23 +1,78 @@
+import glob
+import os
 import pytest
 import subprocess
+import sys
 
 @pytest.mark.parametrize('wasm_name', [
     'sgx-dnet',
     'sgxwallet',
     'SGXCryptoFile',
     'verifiable-election',
-    'sgx-log',
+    # 'sgx-log', # out-of-bound memory access
     'sgx-kmeans',
     # 'sgx-reencrypt', # fail to extract wat
     # 'CryptoEnclave', # fail to extract wat
-    'sgx-pwenclave',
-    'sgx-deep-learning',
+    # 'sgx-pwenclave', # out-of-bound memory access
+    # 'sgx-deep-learning', # z3.z3types.Z3Exception: b'Sorts (_ BitVec 32) and (_ BitVec 64) are incompatible'
     'sgx-biniax2',
-    'sgx-rsa',
-    'sgx_protect_file',
+    # 'sgx-rsa', # out-of-bound memory access
+    # 'sgx_protect_file', # out-of-bound memory access
     # 'SGXSSE' # func_DIE error
 ])
 
-def test_wasm_can_be_analyzed(wasm_name):
-    cmd = ['/usr/bin/env', 'bash', 'run.sh', wasm_name, '--max-time', '5']
+def test_sgx_wasm_can_be_analyzed(wasm_name):
+    cmd = ['/usr/bin/env', 'bash', 'run.sh', wasm_name, '--max-time']
+    cmd.append("5")
     subprocess.run(cmd, timeout=60, check=True)
+
+def test_sgx_wasm_can_be_fully_analyzed():
+    cmd = ['/usr/bin/env', 'bash', 'run.sh', 'SGXCryptoFile']
+    subprocess.run(cmd, timeout=30, check=True)
+
+
+@pytest.mark.parametrize('wasm_path, entry', [
+    ('hello_world.wasm', ''),
+    ('hello_world_go.wasm', '_start'),
+    ('hello_world_rust.wasm', ''),
+    ('test.wasm', ''),
+])
+
+def test_wasm_can_be_analyzed(wasm_path, entry):
+    wasm_path = os.path.join("./test/", wasm_path)
+    cmd = [sys.executable, 'main.py', '-f', wasm_path, '-s', '-v', 'info']
+    if entry != "":
+        cmd.extend(['--entry', entry])
+    subprocess.run(cmd, timeout=30, check=True)
+
+def test_return_simulation():
+    wasm_path = './test/test_return.wasm'
+    cmd = [sys.executable, 'main.py', '-f', wasm_path, '-s', '-v', 'info', '--source_type', 'rust']
+    subprocess.run(cmd, timeout=30, check=True)
+
+    result_dir = glob.glob('./log/result/test_return_*')
+    assert len(result_dir) == 1, 'more than one matching results, do you have multiple `test_return*` cases?'
+    result_dir = result_dir[0]
+    state_path = glob.glob(f'{result_dir}/state*.json')
+    assert len(state_path) == 1, 'should have only one state output `Exit 0`'
+
+    proc = subprocess.run(['jq', '.Solution.proc_exit', state_path[0]], stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=True)
+    out = proc.stdout.decode('utf-8').strip()
+    expect = '"\\u0000"'
+    assert out == expect, f'expect {expect}, got {out}'
+
+def test_unreachable_simulation():
+    wasm_path = './test/test_unreachable.wasm'
+    cmd = [sys.executable, 'main.py', '-f', wasm_path, '-s', '-v', 'info', '--source_type', 'rust']
+    subprocess.run(cmd, timeout=30, check=True)
+
+    result_dir = glob.glob('./log/result/test_unreachable_*')
+    assert len(result_dir) == 1, 'more than one matching results, do you have multiple `test_unreachable*` cases?'
+    result_dir = result_dir[0]
+    state_path = glob.glob(f'{result_dir}/state*.json')
+    assert len(state_path) == 1, 'should have only one state output `null`'
+
+    proc = subprocess.run(['jq', '.Solution.proc_exit', state_path[0]], stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=True)
+    out = proc.stdout.decode('utf-8').strip()
+    expect = 'null'
+    assert out == expect, f'expect {expect}, got {out}'