[BTC Language] OP_CHECKSIG implementation.

symbolic_execution/hardware/machines/btc_machine.py

@@ -17,6 +17,7 @@ from z3 import (
     is_bool,
     If,
     IntSort,
+    BoolSort,
     BitVecSort,
     RecAddDefinition,
     And,
@@ -25,6 +26,7 @@ from z3 import (
     Or,
     ExprRef,
     Function,
+    BoolVal,
 )
 
 from ..interfaces import (
@@ -283,6 +285,16 @@ class BTCVector:
         """Return self"""
         return self
 
+    def check_sig(pubkeys: list, signatures: list):
+        """Check a list of signatures against a list of public keys."""
+        f = Function("check_sig", IntSort(), IntSort(), BoolSort())
+        ret = f(pubkeys[0].val, signatures[0].val)
+
+        return BTCVector(
+            If(ret == BoolVal(True), BTCVector.BTC_TRUE, BTCVector.BTC_FALSE),
+            If(ret == BoolVal(True), IntVal(1), IntVal(0)),
+        )
+
 
 BTC_VECTOR_1 = BTCVector(IntVal(1), BTCVector._min_bytes_needed(1))
 

symbolic_execution/language/bitcoin/op_codes.py

@@ -13,13 +13,14 @@ from symbolic_execution.program.instruction.hybrid import PickInstruction
 from symbolic_execution.program.instruction.interfaces import IInstruction
 from symbolic_execution.program.instruction.stack_based import (
     ArithmeticOperator,
+    CheckSigInstruction,
     ConditionalJump,
     PushDataOperator,
     StackAlterationOperator,
     SwapDataOperator,
 )
 from symbolic_execution.hardware.machines.btc_machine import BTCVector, BTCMachine
-from z3 import And, Int, Or
+from z3 import And, Int, Or, Function, IntSort
 from Crypto.Hash import RIPEMD160
 
 # Special Bitcoin Fields
@@ -704,23 +705,14 @@ class OpCodes:
                 "symbol": "sha256",
             },
         ),
-        "OP_CODESEPARATOR": OpCode(
-            "OP_CODESEPARATOR",
-            instruction_constructor=InvalidInstruction,
-            default_args={
-                "token": "OP_CODESEPARATOR",
-                "tag": InstructionTag.NOT_IMPLEMENTED,
-            },
-        ),
-        # TODO implement crypto
+        "OP_CODESEPARATOR": OpCode("OP_CODESEPARATOR", instruction_constructor=NOP),
         "OP_CHECKSIG": OpCode(
             "OP_CHECKSIG",
-            instruction_constructor=InvalidInstruction,
-            default_args={
-                "token": "OP_CHECKSIG",
-                "tag": InstructionTag.NOT_IMPLEMENTED,
-            },
+            instruction_constructor=CheckSigInstruction,
+            default_args={"sig_function": BTCVector.check_sig},
         ),
+        # TODO implementing multisig requires to support symbolic block read
+        # i.e. the ability to read `n` elements from the stack, `n` being symbolic
         "OP_CHECKMULTISIG": OpCode(
             "OP_CHECKMULTISIG",
             instruction_constructor=InvalidInstruction,

symbolic_execution/program/instruction/stack_based.py

@@ -241,3 +241,28 @@ class ConditionalJump(IConditionalBranchingOperator):
     def __repr__(self) -> str:
         """Return the string representation of the instruction."""
         return f"{super().__repr__()}([{self._destination_pcs}])"
+
+
+class CheckSigInstruction(IInstruction):
+    """IInstruction that checks a or several signatures against public keys."""
+
+    def __init__(self, pc: int, sig_function: Callable, **args):
+        """Initialize the check sig instruction."""
+        super().__init__(pc, **args)
+
+        if sig_function is None:
+            raise InstructionInitializationError("The signature function is None.")
+        self._sig_function = sig_function
+
+    def run(self, machine: IStackBasedMachine):
+        """Check a or several signatures against public keys."""
+        super().run(machine)
+
+        pubkey = machine.pop_from_stack()
+        sig = machine.pop_from_stack()
+
+        machine.push_onto_stack(self._sig_function([pubkey], [sig]))
+
+    def __repr__(self) -> str:
+        """Return the string representation of the instruction."""
+        return f"{super().__repr__()}({'multisig' if self._multisig else 'single_sig'})"