diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 706d4cfab9..21d1a523a6 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -42,7 +42,7 @@ jobs: steps: - name: Install prerequisites run: | - sudo apt install --yes z3 + sudo apt install --yes z3 libsecp256k1-dev - name: Check out code uses: actions/checkout@v3 @@ -76,7 +76,7 @@ jobs: steps: - name: Install prerequisites run: | - sudo apt install --yes z3 + sudo apt install --yes z3 libsecp256k1-dev - name: Check out code uses: actions/checkout@v3 @@ -110,7 +110,7 @@ jobs: steps: - name: Install prerequisites run: | - sudo apt install --yes z3 + sudo apt install --yes z3 libsecp256k1-dev - name: Check out code uses: actions/checkout@v3 diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 77e8311ef2..20be6da98b 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -156,7 +156,7 @@ jobs: steps: - name: Install prerequisites run: | - sudo apt install --yes z3 + sudo apt install --yes z3 libsecp256k1-dev - uses: actions/checkout@v3 with: @@ -196,7 +196,7 @@ jobs: steps: - name: Install prerequisites run: | - sudo apt install --yes z3 + sudo apt install --yes z3 libsecp256k1-dev - uses: actions/checkout@v3 with: @@ -239,7 +239,7 @@ jobs: steps: - name: Install prerequisites run: | - sudo apt install --yes z3 + sudo apt install --yes z3 libsecp256k1-dev - uses: actions/checkout@v3 with: diff --git a/docs/hooks.md b/docs/hooks.md index bb0bee8cc1..2c99c48948 100644 --- a/docs/hooks.md +++ b/docs/hooks.md @@ -905,6 +905,15 @@ Compute the SHA3-256 hash of the input string. [hook{}("KRYPTO.sha3256")] ~~~ +### KRYPTO.ecdsaPubKey + +`ecdsaPubKey` takes a 32-character byte string of a private key, and returns the 64 byte hex-encoded public key. + +~~~ + hooked-symbol ecdsaPubKey{}(String{}) : String{} + [hook{}("KRYPTO.ecdsaPubKey")] +~~~ + ## BYTES Represents a sequence of bytes with update/get/padding operations as well as diff --git a/flake.nix b/flake.nix index 0fbba4e20d..e483c05c0d 100644 --- a/flake.nix +++ b/flake.nix @@ -116,7 +116,7 @@ }; }; nativeBuildInputs = with nixpkgs.legacyPackages.${pkgs.system}; - [ nixpkgs-fmt ] + [ nixpkgs-fmt secp256k1 ] ++ lib.optional (pkgs.system == "aarch64-darwin") pkgs.llvm_12; }; diff --git a/kore/kore.cabal b/kore/kore.cabal index 9e87dfa7ca..af9a763368 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -153,6 +153,7 @@ common library build-depends: process >=1.6 build-depends: profunctors >=5.3 build-depends: recursion-schemes >=5.1 + build-depends: secp256k1-haskell>=0.6 build-depends: semialign >=1 build-depends: sqlite-simple >=0.4 build-depends: stm >=2.5 diff --git a/kore/src/Kore/Builtin/Krypto.hs b/kore/src/Kore/Builtin/Krypto.hs index e2c85086f5..8c454787e7 100644 --- a/kore/src/Kore/Builtin/Krypto.hs +++ b/kore/src/Kore/Builtin/Krypto.hs @@ -43,6 +43,7 @@ import Crypto.Hash ( ) import Crypto.PubKey.ECC.Prim import Crypto.PubKey.ECC.Types +import Crypto.Secp256k1.Internal qualified as Secp256k1 import Data.Bits import Data.ByteString ( ByteString, @@ -61,10 +62,12 @@ import Data.Text qualified as Text import Data.Word ( Word8, ) +import Foreign (alloca, allocaBytes, peek, poke) import Kore.Builtin.Builtin qualified as Builtin import Kore.Builtin.Encoding ( decode8Bit, encode8Bit, + toBase16, ) import Kore.Builtin.Int qualified as Int import Kore.Builtin.String qualified as String @@ -72,9 +75,11 @@ import Kore.Simplify.Simplify ( BuiltinAndAxiomSimplifier, ) import Prelude.Kore +import System.IO.Unsafe (unsafePerformIO) keccak256Key , ecdsaRecoverKey + , ecdsaPubKey , sha256Key , sha512_256RawKey , sha3256Key @@ -82,6 +87,7 @@ keccak256Key IsString s => s keccak256Key = "KRYPTO.keccak256" ecdsaRecoverKey = "KRYPTO.ecdsaRecover" +ecdsaPubKey = "KRYPTO.ecdsaPubKey" sha256Key = "KRYPTO.sha256" sha512_256RawKey = "KRYPTO.sha512_256raw" sha3256Key = "KRYPTO.sha3256" @@ -124,6 +130,7 @@ symbolVerifiers = , (sha512_256RawKey, verifyHashFunction) , (ripemd160Key, verifyHashFunction) , (hashRipemd160Key, verifyHashFunction) + , (ecdsaPubKey, verifyHashFunction) , ( ecdsaRecoverKey , Builtin.verifySymbol @@ -159,6 +166,7 @@ builtinFunctions key | key == ripemd160Key = Just evalRipemd160 | key == hashRipemd160Key = Just evalRipemd160 | key == ecdsaRecoverKey = Just evalECDSARecover + | key == ecdsaPubKey = Just evalECDSAPubKey | key == secp256k1EcdsaRecoverKey = Just evalECDSARecover | otherwise = Nothing @@ -229,6 +237,38 @@ evalSha3256 = evalHashFunction sha3256Key SHA3_256 evalRipemd160 :: BuiltinAndAxiomSimplifier evalRipemd160 = evalHashFunction ripemd160Key RIPEMD160 +secp256k1Ctx :: Secp256k1.Ctx +secp256k1Ctx = unsafePerformIO $ Secp256k1.contextCreate Secp256k1.sign +{-# NOINLINE secp256k1Ctx #-} + +evalECDSAPubKey :: BuiltinAndAxiomSimplifier +evalECDSAPubKey = + Builtin.functionEvaluator evalWorker + where + evalWorker :: Builtin.Function + evalWorker _ resultSort [input] = do + sec_key <- encode8Bit <$> String.expectBuiltinString ecdsaPubKey input + return $ + String.asPattern resultSort $ + if ByteString.length sec_key /= 32 + then "" + else unsafePerformIO $ Secp256k1.unsafeUseByteString sec_key $ \(sec_key_ptr, _) -> allocaBytes 64 $ \pub_key_ptr -> do + createdKeySuccessfully <- + Secp256k1.isSuccess <$> Secp256k1.ecPubKeyCreate secp256k1Ctx pub_key_ptr sec_key_ptr + if not createdKeySuccessfully + then pure "" + else alloca $ \len_ptr -> allocaBytes 65 $ \out_ptr -> do + poke len_ptr 65 + serializedKeySuccessfully <- + Secp256k1.isSuccess + <$> Secp256k1.ecPubKeySerialize secp256k1Ctx out_ptr len_ptr pub_key_ptr Secp256k1.uncompressed + if not serializedKeySuccessfully + then pure "" + else do + final_len <- peek len_ptr + toBase16 . ByteString.tail <$> Secp256k1.packByteString (out_ptr, final_len) + evalWorker _ _ _ = Builtin.wrongArity ecdsaPubKey + evalECDSARecover :: BuiltinAndAxiomSimplifier evalECDSARecover = Builtin.functionEvaluator eval0 diff --git a/test/ecdsa/Makefile b/test/ecdsa/Makefile new file mode 100644 index 0000000000..90a0a30bcd --- /dev/null +++ b/test/ecdsa/Makefile @@ -0,0 +1,3 @@ +DEF = ecdsa +include $(CURDIR)/../include.mk +KOMPILE_OPTS += --hook-namespaces KRYPTO diff --git a/test/ecdsa/addr1.ecdsa b/test/ecdsa/addr1.ecdsa new file mode 100644 index 0000000000..3628ffa30e --- /dev/null +++ b/test/ecdsa/addr1.ecdsa @@ -0,0 +1 @@ +#unparseData(#addrFromPrivateKey("0x2b8ba85ff7f2c7fa62cddb20ae40ef2553b9fdbff086f60d1647ecaab15af867"), 20) diff --git a/test/ecdsa/addr1.ecdsa.out.golden b/test/ecdsa/addr1.ecdsa.out.golden new file mode 100644 index 0000000000..4e1d4d6c32 --- /dev/null +++ b/test/ecdsa/addr1.ecdsa.out.golden @@ -0,0 +1,3 @@ + + "0xd308979bf428e38b458a99da348e28933a4cddb1" ~> . + diff --git a/test/ecdsa/addr2.ecdsa b/test/ecdsa/addr2.ecdsa new file mode 100644 index 0000000000..74514a7f3e --- /dev/null +++ b/test/ecdsa/addr2.ecdsa @@ -0,0 +1 @@ +#unparseData(#addrFromPrivateKey("0x0000000000000000000000000000000000000000000000000000000000000001"), 20) diff --git a/test/ecdsa/addr2.ecdsa.out.golden b/test/ecdsa/addr2.ecdsa.out.golden new file mode 100644 index 0000000000..f10415917c --- /dev/null +++ b/test/ecdsa/addr2.ecdsa.out.golden @@ -0,0 +1,3 @@ + + "0x7e5f4552091a69125d5dfcb7b8c2659029395bdf" ~> . + diff --git a/test/ecdsa/addr3.ecdsa b/test/ecdsa/addr3.ecdsa new file mode 100644 index 0000000000..cbc9bdbb67 --- /dev/null +++ b/test/ecdsa/addr3.ecdsa @@ -0,0 +1 @@ +#unparseData(#addrFromPrivateKey("0x0000000000000000000000000000000000000000000000000000000000000002"), 20) diff --git a/test/ecdsa/addr3.ecdsa.out.golden b/test/ecdsa/addr3.ecdsa.out.golden new file mode 100644 index 0000000000..45ea859deb --- /dev/null +++ b/test/ecdsa/addr3.ecdsa.out.golden @@ -0,0 +1,3 @@ + + "0x2b5ad5c4795c026514f8317c7a215e218dccd6cf" ~> . + diff --git a/test/ecdsa/ecdsa.k b/test/ecdsa/ecdsa.k new file mode 100644 index 0000000000..349e8c78c0 --- /dev/null +++ b/test/ecdsa/ecdsa.k @@ -0,0 +1,85 @@ +module ECDSA + imports INT + imports BYTES + imports STRING + imports BOOL + + syntax String ::= Hex2Raw ( String ) [function] + | Keccak256 ( String ) [function, hook(KRYPTO.keccak256)] + | ECDSAPubKey ( String ) [function, hook(KRYPTO.ecdsaPubKey)] + // ----------------------------------------------- + rule Hex2Raw ( S ) => #unparseByteStack( #parseByteStack ( S ) ) + + syntax Int ::= #addrFromPrivateKey ( String ) [function, klabel(addrFromPrivateKey)] + // ------------------------------------------------------------------------------------ + rule [addrFromPrivateKey]: #addrFromPrivateKey ( KEY ) => #addr( #parseHexWord( Keccak256 ( Hex2Raw ( ECDSAPubKey( Hex2Raw ( KEY ) ) ) ) ) ) + + syntax Int ::= #parseHexWord ( String ) [function] + // -------------------------------------------------- + rule #parseHexWord("") => 0 + rule #parseHexWord("0x") => 0 + rule #parseHexWord(S) => String2Base(replaceAll(S, "0x", ""), 16) requires (S =/=String "") andBool (S =/=String "0x") + + syntax Bytes ::= #parseByteStack ( String ) [function, memo] + | #parseHexBytes ( String ) [function] + | #parseHexBytesAux ( String ) [function] + // -------------------------------------------------------- + rule #parseByteStack(S) => #parseHexBytes(replaceAll(S, "0x", "")) + + rule #parseHexBytes(S) => #parseHexBytesAux(#alignHexString(S)) + rule #parseHexBytesAux("") => .Bytes + rule #parseHexBytesAux(S) => Int2Bytes(lengthString(S) /Int 2, String2Base(S, 16), BE) + requires lengthString(S) >=Int 2 + + syntax String ::= #alignHexString ( String ) [function, total] + // -------------------------------------------------------------- + rule #alignHexString(S) => S requires lengthString(S) modInt 2 ==Int 0 + rule #alignHexString(S) => "0" +String S requires notBool lengthString(S) modInt 2 ==Int 0 + + syntax String ::= #unparseByteStack ( Bytes ) [function, klabel(unparseByteStack), symbol] + // ------------------------------------------------------------------------------------------ + rule #unparseByteStack(WS) => Bytes2String(WS) + + syntax String ::= #unparseData ( Int, Int ) [function] + | #unparseDataBytes ( Bytes ) [function] + // ------------------------------------------------------------ + rule #unparseData( DATA, LENGTH ) => #unparseDataBytes(#padToWidth(LENGTH,#asByteStack(DATA))) + + rule #unparseDataBytes( DATA ) => replaceFirst(Base2String(#asInteger(#asByteStack(1) +Bytes DATA), 16), "1", "0x") + + syntax Int ::= #asInteger ( Bytes ) [function, total] + // ----------------------------------------------------- + rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete] + + syntax Bytes ::= #asByteStack ( Int ) [function, total] + // ------------------------------------------------------- + rule #asByteStack(W) => Int2Bytes(W, BE, Unsigned) [concrete] + + syntax Bytes ::= #padToWidth ( Int , Bytes ) [function, total] + | #padRightToWidth ( Int , Bytes ) [function, total] + // ------------------------------------------------------------------- + rule #padToWidth(N, BS) => BS requires notBool (N >=Int 0) + rule [padToWidthNonEmpty]: #padToWidth(N, BS) => padLeftBytes(BS, N, 0) requires N >=Int 0 + rule #padRightToWidth(N, BS) => BS requires notBool (N >=Int 0) + rule [padRightToWidthNonEmpty]: #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires N >=Int 0 + + syntax Int ::= #addr ( Int ) [function] + // --------------------------------------- + rule #addr(W) => W %Word pow160 + + syntax Int ::= Int "%Word" Int [function, total] + // ------------------------------------------------ + rule _ %Word W1 => 0 requires W1 ==Int 0 + rule W0 %Word W1 => W0 modInt W1 requires W1 =/=Int 0 + + syntax Int ::= "pow160" [alias] /* 2 ^Int 160 */ + // ------------------------------------------------ + rule pow160 => 1461501637330902918203684832716283019655932542976 + + configuration + $PGM:Pgm + + syntax Pgm ::= Bytes | String | Int + // ----------------------------------- + +endmodule