diff --git a/deps/argo b/deps/argo index be9598982f..61c8f59525 160000 --- a/deps/argo +++ b/deps/argo @@ -1 +1 @@ -Subproject commit be9598982f96ed950d94b77be948f49d16a1dc34 +Subproject commit 61c8f59525e13773e31f579cff4d816d76a86796 diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs index 109cb8f97a..c3a8adc77f 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -18,7 +18,7 @@ import SAWServer.SetOption main :: IO () main = - do theApp <- mkApp "SAW RPC Server" serverDocs initialState sawMethods + do theApp <- mkDefaultApp "SAW RPC Server" serverDocs initialState sawMethods defaultMain description theApp serverDocs :: [Doc.Block] diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 4ac421b67f..e937381740 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -80,13 +80,14 @@ instance Show SAWTask where data CrucibleSetupVal e = NullValue | ArrayValue [CrucibleSetupVal e] + | StructValue [CrucibleSetupVal e] -- | TupleValue [CrucibleSetupVal e] -- | RecordValue [(String, CrucibleSetupVal e)] | FieldLValue (CrucibleSetupVal e) String | ElementLValue (CrucibleSetupVal e) Int | GlobalInitializer String | GlobalLValue String - | ServerValue ServerName + | NamedValue ServerName | CryptolExpr e deriving stock (Foldable, Functor, Traversable) diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs index 1586efa24d..cea0b7e921 100644 --- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs +++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs @@ -9,10 +9,11 @@ import Data.Aeson (FromJSON(..), withObject, withText, (.:)) import SAWServer data SetupValTag - = TagServerValue + = TagNamedValue | TagNullValue | TagCryptol | TagArrayValue + | TagStructValue | TagFieldLValue | TagElemLValue | TagGlobalInit @@ -22,11 +23,12 @@ instance FromJSON SetupValTag where parseJSON = withText "tag for setup value" $ \case - "saved" -> pure TagServerValue - "null value" -> pure TagNullValue + "named" -> pure TagNamedValue + "null" -> pure TagNullValue "Cryptol" -> pure TagCryptol - "array value" -> pure TagArrayValue - "field lvalue" -> pure TagFieldLValue + "array" -> pure TagArrayValue + "struct" -> pure TagStructValue + "field" -> pure TagFieldLValue "element lvalue" -> pure TagElemLValue "global initializer" -> pure TagGlobalInit "global lvalue" -> pure TagGlobalLValue @@ -38,10 +40,11 @@ instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where fromObject = withObject "saved value or Cryptol expression" $ \o -> o .: "setup value" >>= \case - TagServerValue -> ServerValue <$> o .: "name" + TagNamedValue -> NamedValue <$> o .: "name" TagNullValue -> pure NullValue TagCryptol -> CryptolExpr <$> o .: "expression" TagArrayValue -> ArrayValue <$> o .: "elements" + TagStructValue -> StructValue <$> o .: "fields" TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field" TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index" TagGlobalInit -> GlobalInitializer <$> o .: "name" diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 0710ea619c..3780ae2165 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -147,7 +147,7 @@ interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty, getSetupVal _ (GlobalLValue name) = JVMSetupM $ return $ MS.SetupGlobal () name -} - getSetupVal (env, _) (ServerValue n) = JVMSetupM $ + getSetupVal (env, _) (NamedValue n) = JVMSetupM $ resolve env n >>= \case Val x -> return x -- TODO add cases for the server values that diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 87dc13a777..8c217685d6 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -33,7 +33,7 @@ import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) import qualified Text.LLVM.AST as LLVM import qualified Data.LLVM.BitCode as LLVM -import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) +import qualified SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) import SAWScript.Crucible.LLVM.Builtins ( llvm_alloc , llvm_alloc_aligned @@ -75,7 +75,7 @@ instance FromJSON StartLLVMCrucibleSetupParams where withObject "params for \"SAW/Crucible setup\"" $ \o -> StartLLVMCrucibleSetupParams <$> o .: "name" -data ServerSetupVal = Val (CMS.AllLLVM SetupValue) +data ServerSetupVal = Val (CMS.AllLLVM MS.SetupValue) -- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now. compileLLVMContract :: @@ -147,6 +147,9 @@ interpretLLVMSetup fileReader bic cenv0 ss = getSetupVal env (ArrayValue elts) = do elts' <- mapM (getSetupVal env) elts LLVMCrucibleSetupM $ return $ CMS.anySetupArray elts' + getSetupVal env (StructValue elts) = + do elts' <- mapM (getSetupVal env) elts + LLVMCrucibleSetupM $ return $ CMS.anySetupStruct False elts' getSetupVal env (FieldLValue base fld) = do base' <- getSetupVal env base LLVMCrucibleSetupM $ return $ CMS.anySetupField base' fld @@ -157,10 +160,10 @@ interpretLLVMSetup fileReader bic cenv0 ss = LLVMCrucibleSetupM $ return $ CMS.anySetupGlobalInitializer name getSetupVal _ (GlobalLValue name) = LLVMCrucibleSetupM $ return $ CMS.anySetupGlobal name - getSetupVal (env, _) (ServerValue n) = LLVMCrucibleSetupM $ + getSetupVal (env, _) (NamedValue n) = LLVMCrucibleSetupM $ resolve env n >>= \case - Val x -> return x -- TODO add cases for the server values that + Val x -> return x -- TODO add cases for the named server values that -- are not coming from the setup monad -- (e.g. surrounding context) getSetupVal (_, cenv) (CryptolExpr expr) = LLVMCrucibleSetupM $ diff --git a/saw-remote-api/test-scripts/env_server.py b/saw-remote-api/test-scripts/env_server.py index 131764f613..f7905e0465 100644 --- a/saw-remote-api/test-scripts/env_server.py +++ b/saw-remote-api/test-scripts/env_server.py @@ -5,13 +5,13 @@ def env_connect(): server = os.environ.get('SAW_SERVER') if not server: - server = "cabal new-exec --verbose=0 saw-remote-api" + server = "cabal new-exec --verbose=0 saw-remote-api socket" print("Running: " + server) return conn.connect(server) def env_connect_global(): server = os.environ.get('SAW_SERVER') if not server: - server = "cabal new-exec --verbose=0 saw-remote-api" + server = "cabal new-exec --verbose=0 saw-remote-api socket" print("Running: " + server) saw.connect(server) diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.cry b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.cry new file mode 100644 index 0000000000..58378f4512 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.cry @@ -0,0 +1,72 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +module HMAC where + +import SHA256 + +//////// Functional version //////// + +hmacSHA256 : {pwBytes, msgBytes} + (fin pwBytes, fin msgBytes + , 32 >= width msgBytes + , 64 >= width (8*pwBytes) + , 64 >= width (8 * (64 + msgBytes)) + ) => [pwBytes][8] -> [msgBytes][8] -> [256] +hmacSHA256 = hmac `{blockLength=64} SHA256 SHA256 SHA256 + +kinit : { pwBytes, blockLength, digest } + ( fin pwBytes, fin blockLength, fin digest ) + => ([pwBytes][8] -> [8*digest]) + -> [pwBytes][8] + -> [blockLength][8] +kinit hash key = + if `pwBytes > (`blockLength : [max (width pwBytes) (width blockLength)]) + then take `{blockLength} (split (hash key) # (zero : [blockLength][8])) + else take `{blockLength} (key # (zero : [blockLength][8])) + +// Due to limitations of the type system we must accept two +// separate arguments (both aledgedly the same) for two +// separate length inputs. +hmac : { msgBytes, pwBytes, digest, blockLength } + ( fin pwBytes, fin digest, fin blockLength ) + => ([blockLength + msgBytes][8] -> [8*digest]) + -> ([blockLength + digest][8] -> [8*digest]) + -> ([pwBytes][8] -> [8*digest]) + -> [pwBytes][8] + -> [msgBytes][8] + -> [digest*8] +hmac hash hash2 hash3 key message = hash2 (okey # internal) + where + ks : [blockLength][8] + ks = kinit hash3 key + okey = [k ^ 0x5C | k <- ks] + ikey = [k ^ 0x36 | k <- ks] + internal = split (hash (ikey # message)) + + + + + + + + + diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.py b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.py new file mode 100644 index 0000000000..d93049516d --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.py @@ -0,0 +1,433 @@ +import os +import os.path +from cryptol.cryptoltypes import to_cryptol +from saw import * +from saw.llvm import Contract, LLVMType, LLVMArrayType, uint8_t, uint32_t, void, SetupVal, FreshVar, cryptol, struct +import saw.llvm_types as ty +from env_server import * + +# N.B., transliteration from HMAC.saw + +dir_path = os.path.dirname(os.path.realpath(__file__)) +c = env_connect() + +# import "HMAC_iterative.cry"; +cryptol_load_file(os.path.join(dir_path, 'HMAC_iterative.cry')) +# import "Hashing.cry"; +cryptol_load_file(os.path.join(dir_path, 'Hashing.cry')) + +################################ +# Generic Utilities. + +# let ptr_to_fresh n ty = do { +# x <- crucible_fresh_var n ty; +# p <- alloc_init ty (crucible_term x); +# return (x, p); +# }; +def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, *, read_only : bool = False) -> Tuple[FreshVar, SetupVal]: + """Add to``Contract`` ``c`` an allocation of a pointer of type ``ty`` initialized to an unknown fresh value. + + :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh + variable will be assigned ``name`` if provided/available.)""" + var = c.declare_var(ty, name) + ptr = c.alloc(c, ty, points_to=var, read_only=read_only) + return (var, ptr) + +# TODO(AMK) Um... what is this: +# let z3_hash_unint = +# w4_unint_z3 [ "hash_init_c_state" +# , "hash_update_c_state" +# , "hash_update_c_state_unbounded" +# , "hash_digest_c_state" +# ]; + +# //////////////////////////////////////////////////////////////// +# // Hash. +# // + +# let setup_hash_state pstate = do { +# alg0 <- crucible_fresh_var "alg" (llvm_int 32); +# h0 <- crucible_fresh_var "h" (llvm_array 8 (llvm_int 64)); +# Nl0 <- crucible_fresh_var "Nl" (llvm_int 64); +# Nh0 <- crucible_fresh_var "Nh" (llvm_int 64); +# u0 <- crucible_fresh_var "u" (llvm_array 16 (llvm_int 64)); +# num0 <- crucible_fresh_var "num" (llvm_int 32); +# is_ready_for_input0 <- crucible_fresh_var "is_ready_for_input" (llvm_int 8); +# currently_in_hash0 <- crucible_fresh_var "currently_in_hash" (llvm_int 64); +# md_len0 <- crucible_fresh_var "md_len" (llvm_int 32); +# (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_struct "struct.s2n_hash"); +# crucible_points_to pstate +# (crucible_struct +# [ pimpl +# , crucible_term alg0 +# , crucible_term is_ready_for_input0 +# , crucible_term currently_in_hash0 +# , crucible_struct +# [ crucible_struct +# [ crucible_struct +# [ crucible_term h0 +# , crucible_term Nl0 +# , crucible_term Nh0 +# , crucible_struct [ crucible_term u0 ] +# , crucible_term num0 +# , crucible_term md_len0 +# ] +# ] +# ] +# ]); +# let st = {{ +# { h = h0 +# , Nl = Nl0 +# , Nh = Nh0 +# , u = u0 +# , num = num0 +# , md_len = md_len0 +# } +# }}; +# return (st, currently_in_hash0); +# }; + + +def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]: + alg0 = c.fresh_var(ty.i32, "alg") + h0 = c.fresh_var(ty.array(8, ty.i64), "h0") + Nl0 = c.fresh_var(ty.i64, "Nl") + Nh0 = c.fresh_var(ty.i64, "Nh") + u0 = c.fresh_var(ty.array(16, ty.i64), "u") + num0 = c.fresh_var(ty.i32, "h0") + is_ready_for_input0 = c.fresh_var(ty.i8, "is_ready_for_input") + currently_in_hash0 = c.fresh_var(ty.i64, "currently_in_hash") + md_len0 = c.fresh_var(ty.i32, "md_len") + (_, pimpl) = ptr_to_fresh(c, ty.alias('struct.s2n_hash'), "impl", read_only=True) + c.points_to(pstate, + struct( + pimpl, + alg0, + is_ready_for_input0, + currently_in_hash0, + struct(struct(struct(h0, Nl0, Nh0, struct(u0), num0, md_len0)) + ))) + # BOOKMARK +# let st = {{ +# { h = h0 +# , Nl = Nl0 +# , Nh = Nh0 +# , u = u0 +# , num = num0 +# , md_len = md_len0 +# } +# }}; +# return (st, currently_in_hash0); + +# let update_hash_state pstate st = do { +# alg <- crucible_fresh_var "alg" (llvm_int 32); +# is_ready_for_input <- crucible_fresh_var "is_ready_for_input" (llvm_int 8); +# currently_in_hash <- crucible_fresh_var "currently_in_hash" (llvm_int 64); +# (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_struct "struct.s2n_hash"); + +# crucible_points_to pstate +# (crucible_struct +# [ pimpl +# , crucible_term alg +# , crucible_term is_ready_for_input +# , crucible_term currently_in_hash +# , crucible_struct +# [ crucible_struct +# [ crucible_struct +# [ crucible_term {{ st.h }} +# , crucible_term {{ st.Nl }} +# , crucible_term {{ st.Nh }} +# , crucible_struct [ crucible_term {{ st.u }} ] +# , crucible_term {{ st.num }} +# , crucible_term {{ st.md_len }} +# ] +# ] +# ] +# ]); +# }; + +# let hash_init_spec = do { +# pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); +# (st0, _) <- setup_hash_state pstate; +# alg <- crucible_fresh_var "alg" (llvm_int 32); +# crucible_execute_func [pstate, crucible_term alg]; +# // We need to pass in the starting state since many of the bits in +# // the union are unused by many of the hash algorithms. +# let st1 = {{ hash_init_c_state st0 }}; +# update_hash_state pstate st1; +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hash_reset_spec = do { +# pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); +# (st0, _) <- setup_hash_state pstate; +# crucible_execute_func [pstate]; +# let st1 = {{ hash_init_c_state st0 }}; +# update_hash_state pstate st1; +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hash_copy_spec = do { +# pstate1 <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); +# pstate2 <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); +# (st1, _) <- setup_hash_state pstate1; +# (st2, _) <- setup_hash_state pstate2; +# crucible_execute_func [pstate1, pstate2]; +# update_hash_state pstate1 st2; +# update_hash_state pstate2 st2; +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hash_update_spec msg_size = do { +# pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); +# (msg, pmsg) <- ptr_to_fresh_readonly "msg" (llvm_array msg_size (llvm_int 8)); +# (st0, _) <- setup_hash_state pstate; +# let size = crucible_term {{ `msg_size : [32] }}; +# crucible_execute_func [pstate, pmsg, size]; +# let st1 = {{ hash_update_c_state`{msg_size=msg_size} st0 msg }}; +# update_hash_state pstate st1; +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hash_update_unbounded_spec = do { +# pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); +# (st0, _) <- setup_hash_state pstate; + +# size <- crucible_fresh_var "size" (llvm_int 32); +# pmsg <- crucible_symbolic_alloc true 1 {{ (0 # size) : [64] }}; +# msg <- crucible_fresh_cryptol_var "msg" {| ByteArray |}; +# crucible_points_to_array_prefix pmsg msg {{ (0 # size) : [64] }}; + +# crucible_execute_func [pstate, pmsg, (crucible_term size)]; + +# let st1 = {{ hash_update_c_state_unbounded st0 msg size }}; +# update_hash_state pstate st1; + +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hash_digest_spec digest_size = do { +# pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); +# (dgst, pdgst) <- ptr_to_fresh "out" (llvm_array digest_size (llvm_int 8)); +# (st0, _) <- setup_hash_state pstate; +# size <- crucible_fresh_var "size" (llvm_int 32); +# crucible_execute_func [pstate, pdgst, crucible_term size]; +# update_hash_state pstate st0; +# let out1 = {{ hash_digest_c_state`{digest_size=digest_size} st0 }}; +# crucible_points_to pdgst (crucible_term out1); +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hash_get_currently_in_hash_total_spec = do { +# pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); +# pout <- crucible_alloc (llvm_int 64); +# (st0, currently_in_hash) <- setup_hash_state pstate; +# crucible_execute_func [pstate, pout]; +# update_hash_state pstate st0; +# crucible_points_to pout (crucible_term {{zero: [64]}} ); +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# //////////////////////////////////////////////////////////////// +# // HMAC. + +# let setup_hmac_state alg0 hash_block_size0 block_size0 digest_size0 = do { +# pstate <- crucible_alloc (llvm_struct "struct.s2n_hmac_state"); +# currently_in_hash_block0 <- crucible_fresh_var "currently_in_hash_block" (llvm_int 32); +# xor_pad0 <- crucible_fresh_var "xor_pad" (llvm_array 128 (llvm_int 8)); +# let digest_size = eval_size {| SHA512_DIGEST_LENGTH |}; +# digest_pad0 <- crucible_fresh_var "digest_pad" (llvm_array digest_size (llvm_int 8)); + +# crucible_points_to (crucible_field pstate "alg") (crucible_term alg0); +# crucible_points_to (crucible_field pstate "hash_block_size") (crucible_term hash_block_size0); +# crucible_points_to (crucible_field pstate "currently_in_hash_block") (crucible_term currently_in_hash_block0); +# crucible_points_to (crucible_field pstate "xor_pad_size") (crucible_term block_size0); +# crucible_points_to (crucible_field pstate "digest_size") (crucible_term digest_size0); +# (inner0, _) <- setup_hash_state (crucible_field pstate "inner"); +# (inner_just_key0, _) <- setup_hash_state (crucible_field pstate "inner_just_key"); +# (outer_just_key0, _) <- setup_hash_state (crucible_field pstate "outer_just_key"); +# (outer0, _) <- setup_hash_state (crucible_field pstate "outer"); +# crucible_points_to (crucible_field pstate "xor_pad") (crucible_term xor_pad0); +# crucible_points_to (crucible_field pstate "digest_pad") (crucible_term digest_pad0); + +# let st0 = {{ +# { alg = alg0 +# , hash_block_size = hash_block_size0 +# , currently_in_hash_block = currently_in_hash_block0 +# , block_size = block_size0 +# , digest_size = digest_size0 +# , inner = inner0 +# , inner_just_key = inner_just_key0 +# , outer = outer0 +# , outer_just_key = outer_just_key0 +# , xor_pad = xor_pad0 +# , digest_pad = digest_pad0 +# } +# }}; +# return (pstate, st0); +# }; + +# let check_hmac_state pstate st = do { +# crucible_points_to (crucible_field pstate "alg") (crucible_term {{ st.alg }}); +# crucible_points_to (crucible_field pstate "hash_block_size") (crucible_term {{ st.hash_block_size }}); +# crucible_points_to (crucible_field pstate "currently_in_hash_block") (crucible_term {{ st.currently_in_hash_block }}); +# crucible_points_to (crucible_field pstate "xor_pad_size") (crucible_term {{ st.block_size }}); +# crucible_points_to (crucible_field pstate "digest_size") (crucible_term {{ st.digest_size }}); +# update_hash_state (crucible_field pstate "inner") {{ st.inner }}; +# update_hash_state (crucible_field pstate "inner_just_key") {{ st.inner_just_key }}; + +# // XXX: Don't care about 'outer' because it gets overwritten by +# // 's2n_hash_reset' before use in 's2n_hmac_digest'. +# // +# //update_hash_state (crucible_elem pstate 7) {{ st.outer }}; +# update_hash_state (crucible_field pstate "outer_just_key") ({{ st.outer_just_key }}); +# crucible_points_to (crucible_field pstate "xor_pad") (crucible_term {{ st.xor_pad }}); + +# // Don't care about 'digest_pad', because it gets overwritten +# // using 's2n_hash_digest' before use in 's2n_hmac_digest'. +# // +# // However, if we leave it in, the proof still goes through +# // (since we model exactly what happens). +# // +# //crucible_points_to (crucible_elem pstate 9) (crucible_term {{ st.digest_pad }}); +# }; + +# let hmac_invariants +# st +# (cfg : { name : String +# , hmac_alg : Term +# , digest_size : Int +# , block_size : Int +# , hash_block_size : Int +# }) = do { +# // Specify the HMAC algorithm. +# crucible_equal (crucible_term {{ st.alg }}) (crucible_term cfg.hmac_alg); + +# // Specify sizes +# let hash_block_size = cfg.hash_block_size; +# let block_size = cfg.block_size; +# let digest_size = cfg.digest_size; +# crucible_equal (crucible_term {{ st.hash_block_size }}) (crucible_term {{ `hash_block_size : [16] }}); +# crucible_equal (crucible_term {{ st.block_size }}) (crucible_term {{ `block_size : [16] }}); +# crucible_equal (crucible_term {{ st.digest_size }}) (crucible_term {{ `digest_size : [8] }}); +# }; + +# //////////////////////////////////////////////////////////////// + +# let hmac_init_spec +# (cfg : { name : String +# , hmac_alg : Term +# , digest_size : Int +# , block_size : Int +# , hash_block_size : Int +# }) = do { +# alg0 <- crucible_fresh_var "alg" (llvm_int 32); +# hash_block_size0 <- crucible_fresh_var "hash_block_size" (llvm_int 16); +# block_size0 <- crucible_fresh_var "block_size" (llvm_int 16); +# digest_size0 <- crucible_fresh_var "digest_size" (llvm_int 8); +# (pstate, st0) <- setup_hmac_state alg0 hash_block_size0 block_size0 digest_size0; + +# klen <- crucible_fresh_var "klen" (llvm_int 32); +# pkey <- crucible_symbolic_alloc true 1 {{ (0 # klen) : [64] }}; +# key <- crucible_fresh_cryptol_var "key" {| ByteArray |}; +# crucible_points_to_array_prefix pkey key {{ (0 # klen) : [64] }}; + +# crucible_execute_func [pstate, crucible_term (cfg.hmac_alg), pkey, (crucible_term klen)]; + +# let block_size = cfg.block_size; +# let hash_block_size = cfg.hash_block_size; +# let digest_size = cfg.digest_size; +# let alg0 = cfg.hmac_alg; + +# let st1 = {{ +# hmac_init_c_state_unbounded +# `{block_size=block_size +# ,hash_block_size=hash_block_size +# ,digest_size=digest_size} +# st0 alg0 key klen +# }}; +# check_hmac_state pstate st1; +# hmac_invariants st1 cfg; +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hmac_update_spec +# (cfg : { name : String +# , hmac_alg : Term +# , digest_size : Int +# , block_size : Int +# , hash_block_size : Int +# }) = do { +# let digest_size = cfg.digest_size; +# let block_size = cfg.block_size; +# let hash_block_size = cfg.hash_block_size; +# (pstate, st0) <- setup_hmac_state +# cfg.hmac_alg +# {{ `hash_block_size : [16] }} +# {{ `block_size : [16] }} +# {{ `digest_size : [8] }}; + +# hmac_invariants st0 cfg; + +# size <- crucible_fresh_var "size" (llvm_int 32); +# pmsg <- crucible_symbolic_alloc true 1 {{ (0 # size) : [64] }}; +# msg <- crucible_fresh_cryptol_var "msg" {| ByteArray |}; +# crucible_points_to_array_prefix pmsg msg {{ (0 # size) : [64] }}; + +# crucible_execute_func [pstate, pmsg, (crucible_term size)]; + +# let st1 = {{ hmac_update_c_state_unbounded st0 msg size }}; +# check_hmac_state pstate st1; +# hmac_invariants st1 cfg; + +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hmac_digest_spec +# (cfg : { name : String +# , hmac_alg : Term +# , digest_size : Int +# , block_size : Int +# , hash_block_size : Int +# }) = do { +# (out, pout) <- ptr_to_fresh "out" (llvm_array cfg.digest_size (llvm_int 8)); + +# let digest_size = cfg.digest_size; +# let block_size = cfg.block_size; +# let hash_block_size = cfg.hash_block_size; +# (pstate, st0) <- setup_hmac_state +# cfg.hmac_alg +# {{ `hash_block_size : [16] }} +# {{ `block_size : [16] }} +# {{ `digest_size : [8] }}; + +# hmac_invariants st0 cfg; + +# let hash_block_size = cfg.hash_block_size; +# let block_size = cfg.block_size; +# let digest_size = cfg.digest_size; +# let size = {{ `digest_size : [32] }}; +# crucible_execute_func [pstate, pout, crucible_term size]; +# let st1_digest = {{ +# hmac_digest_c_state`{block_size=block_size,digest_size=digest_size} st0 +# }}; +# let st1 = {{ st1_digest.0 }}; +# let digest = {{ split (st1_digest.1) : [digest_size][8] }}; + +# crucible_points_to pout (crucible_term digest); +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; + +# let hmac_digest_size_spec +# (cfg : { name : String +# , hmac_alg : Term +# , digest_size : Int +# , block_size : Int +# , hash_block_size : Int +# }) = do { +# psize <- crucible_alloc (llvm_int 8); +# crucible_execute_func [crucible_term cfg.hmac_alg, psize]; +# let digest_size = cfg.digest_size; +# crucible_points_to psize (crucible_term {{ `digest_size : [8] }}); +# crucible_return (crucible_term {{ 0 : [32] }}); +# }; diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.saw b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.saw new file mode 100644 index 0000000000..11a22257f9 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.saw @@ -0,0 +1,417 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +import "HMAC_iterative.cry"; +import "Hashing.cry"; + +//////////////////////////////////////////////////////////////// +// Generic Utilities. +// + +let alloc_init ty v = do { + p <- crucible_alloc ty; + crucible_points_to p v; + return p; +}; + +let alloc_init_readonly ty v = do { + p <- crucible_alloc_readonly ty; + crucible_points_to p (crucible_term v); + return p; +}; + +let ptr_to_fresh n ty = do { + x <- crucible_fresh_var n ty; + p <- alloc_init ty (crucible_term x); + return (x, p); +}; + +let ptr_to_fresh_readonly n ty = do { + x <- crucible_fresh_var n ty; + p <- alloc_init_readonly ty x; + return (x, p); +}; + +let z3_hash_unint = + w4_unint_z3 [ "hash_init_c_state" + , "hash_update_c_state" + , "hash_update_c_state_unbounded" + , "hash_digest_c_state" + ]; + +//////////////////////////////////////////////////////////////// +// Hash. +// + +let setup_hash_state pstate = do { + alg0 <- crucible_fresh_var "alg" (llvm_int 32); + h0 <- crucible_fresh_var "h" (llvm_array 8 (llvm_int 64)); + Nl0 <- crucible_fresh_var "Nl" (llvm_int 64); + Nh0 <- crucible_fresh_var "Nh" (llvm_int 64); + u0 <- crucible_fresh_var "u" (llvm_array 16 (llvm_int 64)); + num0 <- crucible_fresh_var "num" (llvm_int 32); + is_ready_for_input0 <- crucible_fresh_var "is_ready_for_input" (llvm_int 8); + currently_in_hash0 <- crucible_fresh_var "currently_in_hash" (llvm_int 64); + md_len0 <- crucible_fresh_var "md_len" (llvm_int 32); + (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_struct "struct.s2n_hash"); + crucible_points_to pstate + (crucible_struct + [ pimpl + , crucible_term alg0 + , crucible_term is_ready_for_input0 + , crucible_term currently_in_hash0 + , crucible_struct + [ crucible_struct + [ crucible_struct + [ crucible_term h0 + , crucible_term Nl0 + , crucible_term Nh0 + , crucible_struct [ crucible_term u0 ] + , crucible_term num0 + , crucible_term md_len0 + ] + ] + ] + ]); + let st = {{ + { h = h0 + , Nl = Nl0 + , Nh = Nh0 + , u = u0 + , num = num0 + , md_len = md_len0 + } + }}; + return (st, currently_in_hash0); +}; + +let update_hash_state pstate st = do { + alg <- crucible_fresh_var "alg" (llvm_int 32); + is_ready_for_input <- crucible_fresh_var "is_ready_for_input" (llvm_int 8); + currently_in_hash <- crucible_fresh_var "currently_in_hash" (llvm_int 64); + (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_struct "struct.s2n_hash"); + + crucible_points_to pstate + (crucible_struct + [ pimpl + , crucible_term alg + , crucible_term is_ready_for_input + , crucible_term currently_in_hash + , crucible_struct + [ crucible_struct + [ crucible_struct + [ crucible_term {{ st.h }} + , crucible_term {{ st.Nl }} + , crucible_term {{ st.Nh }} + , crucible_struct [ crucible_term {{ st.u }} ] + , crucible_term {{ st.num }} + , crucible_term {{ st.md_len }} + ] + ] + ] + ]); +}; + +let hash_init_spec = do { + pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); + (st0, _) <- setup_hash_state pstate; + alg <- crucible_fresh_var "alg" (llvm_int 32); + crucible_execute_func [pstate, crucible_term alg]; + // We need to pass in the starting state since many of the bits in + // the union are unused by many of the hash algorithms. + let st1 = {{ hash_init_c_state st0 }}; + update_hash_state pstate st1; + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hash_reset_spec = do { + pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); + (st0, _) <- setup_hash_state pstate; + crucible_execute_func [pstate]; + let st1 = {{ hash_init_c_state st0 }}; + update_hash_state pstate st1; + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hash_copy_spec = do { + pstate1 <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); + pstate2 <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); + (st1, _) <- setup_hash_state pstate1; + (st2, _) <- setup_hash_state pstate2; + crucible_execute_func [pstate1, pstate2]; + update_hash_state pstate1 st2; + update_hash_state pstate2 st2; + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hash_update_spec msg_size = do { + pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); + (msg, pmsg) <- ptr_to_fresh_readonly "msg" (llvm_array msg_size (llvm_int 8)); + (st0, _) <- setup_hash_state pstate; + let size = crucible_term {{ `msg_size : [32] }}; + crucible_execute_func [pstate, pmsg, size]; + let st1 = {{ hash_update_c_state`{msg_size=msg_size} st0 msg }}; + update_hash_state pstate st1; + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hash_update_unbounded_spec = do { + pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); + (st0, _) <- setup_hash_state pstate; + + size <- crucible_fresh_var "size" (llvm_int 32); + pmsg <- crucible_symbolic_alloc true 1 {{ (0 # size) : [64] }}; + msg <- crucible_fresh_cryptol_var "msg" {| ByteArray |}; + crucible_points_to_array_prefix pmsg msg {{ (0 # size) : [64] }}; + + crucible_execute_func [pstate, pmsg, (crucible_term size)]; + + let st1 = {{ hash_update_c_state_unbounded st0 msg size }}; + update_hash_state pstate st1; + + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hash_digest_spec digest_size = do { + pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); + (dgst, pdgst) <- ptr_to_fresh "out" (llvm_array digest_size (llvm_int 8)); + (st0, _) <- setup_hash_state pstate; + size <- crucible_fresh_var "size" (llvm_int 32); + crucible_execute_func [pstate, pdgst, crucible_term size]; + update_hash_state pstate st0; + let out1 = {{ hash_digest_c_state`{digest_size=digest_size} st0 }}; + crucible_points_to pdgst (crucible_term out1); + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hash_get_currently_in_hash_total_spec = do { + pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state"); + pout <- crucible_alloc (llvm_int 64); + (st0, currently_in_hash) <- setup_hash_state pstate; + crucible_execute_func [pstate, pout]; + update_hash_state pstate st0; + crucible_points_to pout (crucible_term {{zero: [64]}} ); + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +//////////////////////////////////////////////////////////////// +// HMAC. + +let setup_hmac_state alg0 hash_block_size0 block_size0 digest_size0 = do { + pstate <- crucible_alloc (llvm_struct "struct.s2n_hmac_state"); + currently_in_hash_block0 <- crucible_fresh_var "currently_in_hash_block" (llvm_int 32); + xor_pad0 <- crucible_fresh_var "xor_pad" (llvm_array 128 (llvm_int 8)); + let digest_size = eval_size {| SHA512_DIGEST_LENGTH |}; + digest_pad0 <- crucible_fresh_var "digest_pad" (llvm_array digest_size (llvm_int 8)); + + crucible_points_to (crucible_field pstate "alg") (crucible_term alg0); + crucible_points_to (crucible_field pstate "hash_block_size") (crucible_term hash_block_size0); + crucible_points_to (crucible_field pstate "currently_in_hash_block") (crucible_term currently_in_hash_block0); + crucible_points_to (crucible_field pstate "xor_pad_size") (crucible_term block_size0); + crucible_points_to (crucible_field pstate "digest_size") (crucible_term digest_size0); + (inner0, _) <- setup_hash_state (crucible_field pstate "inner"); + (inner_just_key0, _) <- setup_hash_state (crucible_field pstate "inner_just_key"); + (outer_just_key0, _) <- setup_hash_state (crucible_field pstate "outer_just_key"); + (outer0, _) <- setup_hash_state (crucible_field pstate "outer"); + crucible_points_to (crucible_field pstate "xor_pad") (crucible_term xor_pad0); + crucible_points_to (crucible_field pstate "digest_pad") (crucible_term digest_pad0); + + let st0 = {{ + { alg = alg0 + , hash_block_size = hash_block_size0 + , currently_in_hash_block = currently_in_hash_block0 + , block_size = block_size0 + , digest_size = digest_size0 + , inner = inner0 + , inner_just_key = inner_just_key0 + , outer = outer0 + , outer_just_key = outer_just_key0 + , xor_pad = xor_pad0 + , digest_pad = digest_pad0 + } + }}; + return (pstate, st0); +}; + +let check_hmac_state pstate st = do { + crucible_points_to (crucible_field pstate "alg") (crucible_term {{ st.alg }}); + crucible_points_to (crucible_field pstate "hash_block_size") (crucible_term {{ st.hash_block_size }}); + crucible_points_to (crucible_field pstate "currently_in_hash_block") (crucible_term {{ st.currently_in_hash_block }}); + crucible_points_to (crucible_field pstate "xor_pad_size") (crucible_term {{ st.block_size }}); + crucible_points_to (crucible_field pstate "digest_size") (crucible_term {{ st.digest_size }}); + update_hash_state (crucible_field pstate "inner") {{ st.inner }}; + update_hash_state (crucible_field pstate "inner_just_key") {{ st.inner_just_key }}; + + // XXX: Don't care about 'outer' because it gets overwritten by + // 's2n_hash_reset' before use in 's2n_hmac_digest'. + // + //update_hash_state (crucible_elem pstate 7) {{ st.outer }}; + update_hash_state (crucible_field pstate "outer_just_key") ({{ st.outer_just_key }}); + crucible_points_to (crucible_field pstate "xor_pad") (crucible_term {{ st.xor_pad }}); + + // Don't care about 'digest_pad', because it gets overwritten + // using 's2n_hash_digest' before use in 's2n_hmac_digest'. + // + // However, if we leave it in, the proof still goes through + // (since we model exactly what happens). + // + //crucible_points_to (crucible_elem pstate 9) (crucible_term {{ st.digest_pad }}); +}; + +let hmac_invariants + st + (cfg : { name : String + , hmac_alg : Term + , digest_size : Int + , block_size : Int + , hash_block_size : Int + }) = do { + // Specify the HMAC algorithm. + crucible_equal (crucible_term {{ st.alg }}) (crucible_term cfg.hmac_alg); + + // Specify sizes + let hash_block_size = cfg.hash_block_size; + let block_size = cfg.block_size; + let digest_size = cfg.digest_size; + crucible_equal (crucible_term {{ st.hash_block_size }}) (crucible_term {{ `hash_block_size : [16] }}); + crucible_equal (crucible_term {{ st.block_size }}) (crucible_term {{ `block_size : [16] }}); + crucible_equal (crucible_term {{ st.digest_size }}) (crucible_term {{ `digest_size : [8] }}); +}; + +//////////////////////////////////////////////////////////////// + +let hmac_init_spec + (cfg : { name : String + , hmac_alg : Term + , digest_size : Int + , block_size : Int + , hash_block_size : Int + }) = do { + alg0 <- crucible_fresh_var "alg" (llvm_int 32); + hash_block_size0 <- crucible_fresh_var "hash_block_size" (llvm_int 16); + block_size0 <- crucible_fresh_var "block_size" (llvm_int 16); + digest_size0 <- crucible_fresh_var "digest_size" (llvm_int 8); + (pstate, st0) <- setup_hmac_state alg0 hash_block_size0 block_size0 digest_size0; + + klen <- crucible_fresh_var "klen" (llvm_int 32); + pkey <- crucible_symbolic_alloc true 1 {{ (0 # klen) : [64] }}; + key <- crucible_fresh_cryptol_var "key" {| ByteArray |}; + crucible_points_to_array_prefix pkey key {{ (0 # klen) : [64] }}; + + crucible_execute_func [pstate, crucible_term (cfg.hmac_alg), pkey, (crucible_term klen)]; + + let block_size = cfg.block_size; + let hash_block_size = cfg.hash_block_size; + let digest_size = cfg.digest_size; + let alg0 = cfg.hmac_alg; + + let st1 = {{ + hmac_init_c_state_unbounded + `{block_size=block_size + ,hash_block_size=hash_block_size + ,digest_size=digest_size} + st0 alg0 key klen + }}; + check_hmac_state pstate st1; + hmac_invariants st1 cfg; + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hmac_update_spec + (cfg : { name : String + , hmac_alg : Term + , digest_size : Int + , block_size : Int + , hash_block_size : Int + }) = do { + let digest_size = cfg.digest_size; + let block_size = cfg.block_size; + let hash_block_size = cfg.hash_block_size; + (pstate, st0) <- setup_hmac_state + cfg.hmac_alg + {{ `hash_block_size : [16] }} + {{ `block_size : [16] }} + {{ `digest_size : [8] }}; + + hmac_invariants st0 cfg; + + size <- crucible_fresh_var "size" (llvm_int 32); + pmsg <- crucible_symbolic_alloc true 1 {{ (0 # size) : [64] }}; + msg <- crucible_fresh_cryptol_var "msg" {| ByteArray |}; + crucible_points_to_array_prefix pmsg msg {{ (0 # size) : [64] }}; + + crucible_execute_func [pstate, pmsg, (crucible_term size)]; + + let st1 = {{ hmac_update_c_state_unbounded st0 msg size }}; + check_hmac_state pstate st1; + hmac_invariants st1 cfg; + + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hmac_digest_spec + (cfg : { name : String + , hmac_alg : Term + , digest_size : Int + , block_size : Int + , hash_block_size : Int + }) = do { + (out, pout) <- ptr_to_fresh "out" (llvm_array cfg.digest_size (llvm_int 8)); + + let digest_size = cfg.digest_size; + let block_size = cfg.block_size; + let hash_block_size = cfg.hash_block_size; + (pstate, st0) <- setup_hmac_state + cfg.hmac_alg + {{ `hash_block_size : [16] }} + {{ `block_size : [16] }} + {{ `digest_size : [8] }}; + + hmac_invariants st0 cfg; + + let hash_block_size = cfg.hash_block_size; + let block_size = cfg.block_size; + let digest_size = cfg.digest_size; + let size = {{ `digest_size : [32] }}; + crucible_execute_func [pstate, pout, crucible_term size]; + let st1_digest = {{ + hmac_digest_c_state`{block_size=block_size,digest_size=digest_size} st0 + }}; + let st1 = {{ st1_digest.0 }}; + let digest = {{ split (st1_digest.1) : [digest_size][8] }}; + + crucible_points_to pout (crucible_term digest); + crucible_return (crucible_term {{ 0 : [32] }}); +}; + +let hmac_digest_size_spec + (cfg : { name : String + , hmac_alg : Term + , digest_size : Int + , block_size : Int + , hash_block_size : Int + }) = do { + psize <- crucible_alloc (llvm_int 8); + crucible_execute_func [crucible_term cfg.hmac_alg, psize]; + let digest_size = cfg.digest_size; + crucible_points_to psize (crucible_term {{ `digest_size : [8] }}); + crucible_return (crucible_term {{ 0 : [32] }}); +}; diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_append_correct.saw b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_append_correct.saw new file mode 100644 index 0000000000..0fc6bcf10d --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_append_correct.saw @@ -0,0 +1,80 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +import "HMAC_properties.cry"; +import "modthm.cry"; + +let hash_lemma1 = + rewrite (cryptol_ss ()) (unfold_term ["hash_update_append"] {{ hash_update_append }}); + +let hash_lemma2 = + rewrite (cryptol_ss ()) (unfold_term ["hash_update_empty"] {{ hash_update_empty }}); + +let mod_lemma = rewrite (cryptol_ss ()) (unfold_term ["modthm"] {{ modthm }}); + +let tuple_lemma = rewrite (cryptol_ss ()) (unfold_term ["modthm"] {{ modthm }}); + +let tuple_lemma = rewrite (cryptol_ss ()) {{ + \a1 b1 c1 d1 a2 b2 c2 d2 -> + ((a1,b1,c1,d1) == (a2,b2,c2,d2)) == (a1 == a2 /\ b1 == b2 /\ c1 == c2 /\ d1 == d2) +}}; + +let eq_lemma = rewrite (cryptol_ss ()) {{ + \a -> (a == a) == True +}}; + +let and_true1 = rewrite (cryptol_ss ()) {{ + \a -> (a /\ True) == a +}}; + +let and_true2 = rewrite (cryptol_ss ()) {{ + \a -> (True /\ a) == a +}}; + +let {{ +type_add_lemma : {a,b} (fin a, fin b, 32 >= width a, 32 >= width b, 32 >= width (a + b)) => Bit +type_add_lemma = (`(a + b) : [32]) == ((`b : [32]) + (`a : [32])) +}}; + +let type_add_lemma = rewrite (cryptol_ss()) (unfold_term ["type_add_lemma"] {{ type_add_lemma }}); + +and_true1_thm <- time (prove_print abc and_true1); +and_true2_thm <- time (prove_print abc and_true2); + +time (prove_print (do { + unfolding ["hmac_update_append"]; + unfolding ["hmac_update_c_state"]; + simplify (cryptol_ss ()); + simplify (addsimps' [hash_lemma1, mod_lemma, tuple_lemma, eq_lemma] empty_ss); + simplify (addsimps [and_true1_thm, and_true2_thm] empty_ss); + simplify (addsimps' [type_add_lemma] empty_ss); + simplify (add_prelude_eqs ["eq_refl"] empty_ss); + simplify (addsimps' [eq_lemma] empty_ss); + trivial; +}) {{ hmac_update_append }}); + +time (prove_print (do { + unfolding ["hmac_update_empty"]; + unfolding ["hmac_update_c_state"]; + simplify(cryptol_ss ()); + simplify (addsimp' hash_lemma2 empty_ss); + unint_yices ["hash_update_c_state"]; +}) {{ hmac_update_empty }}); diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_imp_correct.saw b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_imp_correct.saw new file mode 100644 index 0000000000..33811dfdab --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_imp_correct.saw @@ -0,0 +1,29 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +import "HMAC.cry"; + +let check n = do { + print (str_concat "Checking 'hmac_imp_correct' for byte count " (show n)); + time (prove_print abc {{ hmac_imp_correct : [n][8] -> [n][8] -> Bit }}); +}; + +for [0, 1, 2, 63, 64, 65, 127, 128, 129 /*, 1000 */] check; diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_iterative.cry b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_iterative.cry new file mode 100644 index 0000000000..665bd9a8f0 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_iterative.cry @@ -0,0 +1,399 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +module HMAC_iterative where + +import Array +import SHA256 +import Hashing + +//////////////////////////////////////////////////////////////// +// HMAC (specialized to SHA256). +//////////////////////////////////////////////////////////////// + +// s2n_hmac.h +/* +typedef enum { S2N_HMAC_NONE, S2N_HMAC_MD5, S2N_HMAC_SHA1, S2N_HMAC_SHA224, S2N_HMAC_SHA256, S2N_HMAC_SHA384, + S2N_HMAC_SHA512, S2N_HMAC_SSLv3_MD5, S2N_HMAC_SSLv3_SHA1 +} s2n_hmac_algorithm; +*/ + +S2N_HMAC_NONE = 0:[32] +S2N_HMAC_MD5 = 1:[32] +S2N_HMAC_SHA1 = 2:[32] +S2N_HMAC_SHA224 = 3:[32] +S2N_HMAC_SHA256 = 4:[32] +S2N_HMAC_SHA384 = 5:[32] +S2N_HMAC_SHA512 = 6:[32] +S2N_HMAC_SSLv3_MD5 = 7:[32] +S2N_HMAC_SSLv3_SHA1 = 8:[32] + +// s2n_hmac.h +/* + +struct s2n_hmac_state { + s2n_hmac_algorithm alg; + + uint16_t hash_block_size; + uint32_t currently_in_hash_block; + uint16_t block_size; + uint8_t digest_size; + + struct s2n_hash_state inner; + struct s2n_hash_state inner_just_key; + struct s2n_hash_state outer; + + /* key needs to be as large as the biggest block size */ + uint8_t xor_pad[128]; + + /* For storing the inner digest */ + uint8_t digest_pad[SHA512_DIGEST_LENGTH]; +}; +*/ +// No surprises in the LLVM (:/src/hmac.ll) +/* +%struct.s2n_hmac_state = type { i32, i16, i32, i16, i8, %struct.s2n_hash_state, %struct.s2n_hash_state, %struct.s2n_hash_state, [128 x i8], [64 x i8] } +*/ + +type HMAC_c_state = + { alg : [32] + , hash_block_size : [16] + , currently_in_hash_block : [32] + , block_size : [16] + , digest_size : [8] + , inner : SHA512_c_state + , inner_just_key : SHA512_c_state + , outer : SHA512_c_state + , outer_just_key : SHA512_c_state + , xor_pad : [128][8] + , digest_pad : [SHA512_DIGEST_LENGTH][8] + } + +//////////////////////////////////////////////////////////////// +// Deep HMAC specs in terms of C HMAC state. +// +// Here "deep" because we reimplement the HMAC functions to call the +// corresponding hash functions on the raw C hash states, instead of +// converting them to Cryptol SHA256 hash states. + +type ByteArray = Array[64][8] + +type hash_init_ty = + SHA512_c_state -> SHA512_c_state +type hash_update_ty msg_size = + SHA512_c_state -> [msg_size][8] -> SHA512_c_state +type hash_digest_ty digest_size = + SHA512_c_state -> [digest_size][8] + +hash_init_c_state : hash_init_ty +hash_init_c_state = sha256_init_sha512_c_state +//hash_init_c_state = undefined + +// Cryptol does not support polymorphic arguments (rank 2 +// polymorphism), so making the hash update function a parameter to +// the hmac functions is annoying, since we must pass a separate +// monomorphic copy for each use at a different type. Instead, we just +// define it at the top level, but can leave it uninterpreted in the +// "generic" verification. +hash_update_c_state : + {msg_size} (fin msg_size) => hash_update_ty msg_size +hash_update_c_state = sha256_update_sha512_c_state +//hash_update_c_state = undefined +hash_update_c_state_unbounded : + SHA512_c_state -> ByteArray -> [32] -> SHA512_c_state +hash_update_c_state_unbounded = undefined + + +hash_digest_c_state : + {digest_size} (fin digest_size) => hash_digest_ty digest_size +// To support any digest length, we pad and truncate as necessary. +// This implementation only makes sense for SHA256 size params, but +// that is not a concern since we leave these functions uninterpreted +// in the verification against the S2N C code (we want a concrete +// implementation for debugging and to compare with our functional spec). +hash_digest_c_state st = + take `{digest_size} + (sha256_digest_sha512_c_state st # (zero : [inf][8])) +//hash_digest_c_state = undefined + + +// Cases depending on key size: +// +// * small key (key size <= block size) +// +// copy key into 'xor_pad', up to key size +// +// * large key (key size > block size) +// +// update outer state with key to key size +// digest outer state into digest pad at digest size +// +// The C code that follows the key init sets all remaining bytes, +// up to block size, to 0x36, and xors the other bytes with 0x36. +// This is equivalent to setting upper bytes (i.e. up to block size) +// to zero in key init, and then xoring everything with 0x36. +// +// We don't care about 'xor_pad' and 'outer', so we should be able to +// just ignore them. But for now we just compute them anyway. +key_init_c_state : { key_size, block_size, digest_size } + ( fin key_size, fin block_size, + SHA512_DIGEST_LENGTH >= digest_size ) + => SHA512_c_state + -> [SHA512_DIGEST_LENGTH][8] + -> [key_size][8] + -> (SHA512_c_state, [SHA512_DIGEST_LENGTH][8], [block_size][8]) +key_init_c_state outer0 digest_pad0 key = + if `key_size > (`block_size : [max (width key_size) (width block_size)]) + then (outer2, digest_pad1, hash') + else (outer1, digest_pad0, key') + where + outer1 = hash_init_c_state outer0 + + // Long key. + outer2 = hash_update_c_state outer1 key + hash : [digest_size][8] + hash = hash_digest_c_state outer2 + digest_pad1 = hash # drop `{digest_size} digest_pad0 + hash' = take `{block_size} (hash # (zero : [block_size][8])) + + // Short key. + key' = take `{block_size} (key # (zero : [block_size][8])) + +key_init_c_state_unbounded : { block_size, digest_size } + ( 16 >= width block_size, SHA512_DIGEST_LENGTH >= digest_size ) + => SHA512_c_state + -> [SHA512_DIGEST_LENGTH][8] + -> ByteArray + -> [32] + -> (SHA512_c_state, [SHA512_DIGEST_LENGTH][8], [block_size][8]) +key_init_c_state_unbounded outer0 digest_pad0 key klen = + if klen > (`block_size : [32]) + then (outer2, digest_pad1, hash') + else (outer1, digest_pad0, key') + where + outer1 = hash_init_c_state outer0 + + // Long key. + outer2 = hash_update_c_state_unbounded outer1 key klen + hash : [digest_size][8] + hash = hash_digest_c_state outer2 + digest_pad1 = hash # drop `{digest_size} digest_pad0 + hash' = take `{block_size} (hash # (zero : [block_size][8])) + + // Short key. + key' = map + (\i -> if (i <$ (0 # klen)) then (arrayLookup key i) else 0) + (take`{block_size} [0 .. block_size]) + +hmac_init_c_state : + { key_size, block_size, hash_block_size, digest_size } + ( fin key_size + , 64 >= width (8*key_size) + , 16 >= width hash_block_size + , 16 >= width block_size + , 8 >= width digest_size + , 128 >= block_size + , 64 >= digest_size ) + => HMAC_c_state + -> [32] + -> [key_size][8] + -> HMAC_c_state +hmac_init_c_state st0 alg key = + { alg = alg + , hash_block_size = `hash_block_size + , currently_in_hash_block = currently_in_hash_block + , block_size = `block_size + , digest_size = `digest_size + + , inner = inner + , inner_just_key = inner_just_key + , outer = outer + , outer_just_key = outer_just_key + , xor_pad = xor_pad + , digest_pad = digest_pad + } + where + currently_in_hash_block = 0 + + k0 : [block_size][8] + (outer, digest_pad, k0) = + key_init_c_state `{digest_size=digest_size} st0.outer st0.digest_pad key + ikey = [ k ^ 0x36 | k <- k0 ] + okey = [ k ^ 0x6a | k <- ikey ] + + inner_just_key = hash_update_c_state + (hash_init_c_state st0.inner_just_key) ikey + inner = inner_just_key + outer_just_key = hash_update_c_state + (hash_init_c_state st0.outer_just_key) okey + xor_pad = zero //okey # drop st0.xor_pad + +hmac_init_c_state_unbounded : + { block_size, hash_block_size, digest_size } + ( 16 >= width hash_block_size + , 16 >= width block_size + , 8 >= width digest_size + , 128 >= block_size + , 64 >= digest_size ) + => HMAC_c_state + -> [32] + -> ByteArray + -> [32] + -> HMAC_c_state +hmac_init_c_state_unbounded st0 alg key klen = + { alg = alg + , hash_block_size = `hash_block_size + , currently_in_hash_block = currently_in_hash_block + , block_size = `block_size + , digest_size = `digest_size + + , inner = inner + , inner_just_key = inner_just_key + , outer = outer + , outer_just_key = outer_just_key + , xor_pad = xor_pad + , digest_pad = digest_pad + } + where + currently_in_hash_block = 0 + + k0 : [block_size][8] + (outer, digest_pad, k0) = + key_init_c_state_unbounded `{digest_size=digest_size} + st0.outer st0.digest_pad key klen + ikey = [ k ^ 0x36 | k <- k0 ] + okey = [ k ^ 0x6a | k <- ikey ] + + inner_just_key = hash_update_c_state + (hash_init_c_state st0.inner_just_key) ikey + inner = inner_just_key + outer_just_key = hash_update_c_state + (hash_init_c_state st0.outer_just_key) okey + xor_pad = zero //okey # drop st0.xor_pad + + +hmac_update_c_state : {msg_size} (32 >= width msg_size) => + HMAC_c_state -> [msg_size][8] -> HMAC_c_state +hmac_update_c_state s m = + { inner = hash_update_c_state s.inner m + , currently_in_hash_block = + (s.currently_in_hash_block + (`msg_size % (zero # s.hash_block_size))) % + (zero # s.block_size) + + // Rest unchanged. + , alg = s.alg + , hash_block_size = s.hash_block_size + , block_size = s.block_size + , digest_size = s.digest_size + , inner_just_key = s.inner_just_key + , outer = s.outer + , outer_just_key = s.outer_just_key + , xor_pad = s.xor_pad + , digest_pad = s.digest_pad + } + +hmac_update_c_state_unbounded : + HMAC_c_state -> ByteArray -> [32] -> HMAC_c_state +hmac_update_c_state_unbounded s m sz = + { inner = hash_update_c_state_unbounded s.inner m sz + , currently_in_hash_block = + (s.currently_in_hash_block + (sz % (zero # s.hash_block_size))) % + (zero # s.block_size) + + // Rest unchanged. + , alg = s.alg + , hash_block_size = s.hash_block_size + , block_size = s.block_size + , digest_size = s.digest_size + , inner_just_key = s.inner_just_key + , outer = s.outer + , outer_just_key = s.outer_just_key + , xor_pad = s.xor_pad + , digest_pad = s.digest_pad + } + + +// TODO: What about `size` argument to `s2n_hmac_digest`? The `size` +// argument is supposed to be the "digest length" of the underlying +// hash. Here we are specializing to SHA256, so `size` would be 32. +hmac_digest_c_state : + { block_size, digest_size } + ( 64 >= digest_size + , 128 >= block_size ) + => HMAC_c_state -> (HMAC_c_state, [8 * digest_size]) +hmac_digest_c_state s = (sout, out) + where + hin : [digest_size][8] + hin = hash_digest_c_state inner + digest_pad : [SHA512_DIGEST_LENGTH][8] + digest_pad = hin # zero + + okey : [block_size][8] + okey = take s.xor_pad + + // The `inner` and `outer` here are probably not accurate: + // in s2n, the `s2n_hash_digest` has been called on them, which + // presumably can change them (calls `SHA256_Final` from + // underlying C crypto lib behind the scenes). However, our + // Cryptol `SHA256Final` does not change the hash state. Even + // if we leave the hash function uninterpreted later, we will + // still need to change the interface of our Cryptol `Final` + // to additionally return an updated `State`. + // + // However, we probably don't need to say anything about the + // *hash* state after calls to "final" functions, since + // 's2n_hash_reset' just calls 's2n_hash_init'. So, the above + // concern is not much of a concern after all. + + // Our goal is to leave the hash functions (init, update, + // digest/final) uninterpreted, and so we need the structure of + // our calls to these functions to match the structure of calls in + // the s2n code, since we don't have lemmas giving algebraic + // properties of these functions (e.g. here we'd need + // + // update (update st x) y == update st (x # y) + // + // ). So, we replace + // + //outer = SHA256Update SHA256Init (okey # hin) + // + // with: + outer = hash_update_c_state s.outer_just_key hin + inner = s.inner + + out = join (hash_digest_c_state outer) + + sout : HMAC_c_state + sout = + { inner = inner + , outer = s.outer_just_key + , digest_pad = digest_pad + + // Rest unchanged. + , alg = s.alg + , hash_block_size = s.hash_block_size + , currently_in_hash_block = s.currently_in_hash_block + , block_size = s.block_size + , digest_size = s.digest_size + , inner_just_key = s.inner_just_key + , outer_just_key = s.outer_just_key + , xor_pad = s.xor_pad + } \ No newline at end of file diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_properties.cry b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_properties.cry new file mode 100644 index 0000000000..2ef6672c1f --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC_properties.cry @@ -0,0 +1,104 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +module HMAC_properties where + +import HMAC +import Hashing +import HMAC_iterative + +//////// Equivalence of implementations //////// +// +// This is specialized to SHA256, since we don't have concrete +// implementations of the other algorithms. +hmac_c_state : { key_size, msg_size } + ( 32 >= width msg_size, 64 >= width (8 * key_size) ) + => HMAC_c_state -> [key_size][8] -> [msg_size][8] -> [SHA256_DIGEST_LENGTH * 8] +hmac_c_state st0 key msg = digest + where + (st1, digest) = + hmac_digest_c_state `{block_size=64} + (hmac_update_c_state + (hmac_init_c_state `{block_size=64,hash_block_size=64,digest_size=SHA256_DIGEST_LENGTH} + st0 alg key) + msg) + // Specialize to SHA256. + alg = S2N_HMAC_SHA256 + +hmac_c_state_correct : { key_size, msg_size } + ( 32 >= width msg_size, 64 >= width (8 * key_size) ) + => HMAC_c_state -> [key_size][8] -> [msg_size][8] -> Bit +property hmac_c_state_correct st0 key msg = + hmacSHA256 key msg == hmac_c_state st0 key msg + +hmac_c_state_multi : { key_size, msg_size, msg_chunks} + ( 32 >= width msg_size, 64 >= width (8 * key_size), fin msg_chunks ) + => HMAC_c_state -> [key_size][8] -> [msg_chunks][msg_size][8] -> [SHA256_DIGEST_LENGTH * 8] +hmac_c_state_multi st0 key msgs = digest + where + initial_state = (hmac_init_c_state `{block_size=64,hash_block_size=64,digest_size=SHA256_DIGEST_LENGTH} + st0 alg key) + mid_state = hmac_update_c_state_multi initial_state msgs + (st1, digest) = hmac_digest_c_state `{block_size=64} mid_state + // Specialize to SHA256. + alg = S2N_HMAC_SHA256 + +hmac_update_c_state_multi : {msg_size, msg_chunks} + ( 32 >= width msg_size, fin msg_chunks) + => HMAC_c_state -> [msg_chunks][msg_size][8] -> HMAC_c_state +hmac_update_c_state_multi st msgs = states ! 0 + where + states = [st] # [hmac_update_c_state s msg | msg <- msgs | s <- states] + +hmac_c_state_multi_correct : { key_size, msg_size, msg_chunks } + ( 32 >= width msg_size + , 64 >= width (8 * key_size) + , fin msg_chunks + , 32 >= width (msg_chunks * msg_size) + , 64 >= width (8 * (64 + msg_size * msg_chunks)) + ) + => HMAC_c_state -> [key_size][8] -> [msg_chunks][msg_size][8] -> Bit +property hmac_c_state_multi_correct st0 key msgs = + hmacSHA256 key (join msgs) == hmac_c_state_multi st0 key msgs + +hmac_update_append x y s = + hmac_update_c_state (hmac_update_c_state s x) y == hmac_update_c_state s (x # y) + +hash_update_append x y s = + hash_update_c_state (hash_update_c_state s x) y == hash_update_c_state s (x # y) + +hmac_update_append_init x y k st0 = + hmac_update_c_state (hmac_update_c_state s x) y == hmac_update_c_state s (x # y) + where + s = hmac_init_c_state st0 S2N_HMAC_SHA256 k + +property hash_update_empty s = hash_update_c_state s [] == s + +property hmac_update_empty s = + s.currently_in_hash_block == s.currently_in_hash_block % (zero # s.block_size) + ==> + hmac_update_c_state s [] == s + +property pass = + ~zero == + [ hmacSHA256 [0x0b | _ <- [1..20] : [_][6]] "Hi There" == 0xb0344c61d8db38535ca8afceaf0bf12b881dc200c9833da726e9376c2e32cff7 + , hmacSHA256 "Jefe" "what do ya want for nothing?" == 0x5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843 + ] diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/Hashing.cry b/saw-remote-api/test-scripts/in-progress/HMAC/spec/Hashing.cry new file mode 100644 index 0000000000..fe1e46d9d8 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/Hashing.cry @@ -0,0 +1,224 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +module Hashing where + +import SHA256 + + +//////////////////////////////////////////////////////////////// +// Hashing +//////////////////////////////////////////////////////////////// + +// s2n_hash.h +/* +typedef enum { S2N_HASH_NONE, S2N_HASH_MD5, S2N_HASH_SHA1, S2N_HASH_SHA224, S2N_HASH_SHA256, S2N_HASH_SHA384, + S2N_HASH_SHA512, S2N_HASH_MD5_SHA1 +} s2n_hash_algorithm; +*/ +S2N_HASH_NONE = 0:[32] +S2N_HASH_MD5 = 1:[32] +S2N_HASH_SHA1 = 2:[32] +S2N_HASH_SHA224 = 3:[32] +S2N_HASH_SHA256 = 4:[32] +S2N_HASH_SHA384 = 5:[32] +S2N_HASH_SHA512 = 6:[32] +S2N_HASH_MD5_SHA1 = 7:[32] + +// /usr/include/openssl/sha.h +/* +134 typedef struct SHA256state_st { +135 SHA_LONG h[8]; +136 SHA_LONG Nl, Nh; +137 SHA_LONG data[SHA_LBLOCK]; +138 unsigned int num, md_len; +139 } SHA256_CTX; +*/ +// Looking at the generated LLVM in ':/src/hmac.ll' gives the precise +// layout, without having to find the definitions of the above +// macros. +/* +%struct.SHA512state_st = type { [8 x i64], i64, i64, %union.anon.0, i32, i32 } +%union.anon.0 = type { [16 x i64] } +*/ + +// The hash state in s2n is stored in a union, and the largest member +// of that union is the SHA512 hash state. So, we need to translate +// between SHA512 and SHA256 hash states. +// +// /usr/include/openssl/sha.h +/* +183 typedef struct SHA512state_st { +184 SHA_LONG64 h[8]; +185 SHA_LONG64 Nl, Nh; +186 union { +187 SHA_LONG64 d[SHA_LBLOCK]; +188 unsigned char p[SHA512_CBLOCK]; +189 } u; +190 unsigned int num, md_len; +191 } SHA512_CTX; +*/ +// :/src/hmac.ll +/* +%struct.SHA256state_st = type { [8 x i32], i32, i32, [16 x i32], i32, i32 } +*/ + +type SHA512_c_state = + { h : [8][64] + , Nl : [64] + , Nh : [64] + , u : [16][64] + , num : [32] + , md_len : [32] + } +type SHA512_c_bits = 8*64+64+64+16*64+32+32 + +join512_c_state : SHA512_c_state -> [SHA512_c_bits] +join512_c_state st = join st.h # st.Nl # st.Nh # join st.u # st.num # st.md_len + +type SHA256_c_state = + { h : [8][32] + , Nl : [32] // The low bits of 'sz'. + , Nh : [32] // The high bits of 'sz'. + , u : [16][32] // The 'block': '[16][32] == [8][64]' when flattened. + , num : [32] // The 'n', but extended to 32 bits. + , md_len : [32] // The value of 'md_len' is always 32, + } // i.e. 'SHA256_DIGEST_LENGTH'. +type SHA256_c_bits = 8*32+32+32+16*32+32+32 + +join256_c_state : SHA256_c_state -> [SHA256_c_bits] +join256_c_state st = join st.h # st.Nl # st.Nh # join st.u # st.num # st.md_len + +type SHA256_DIGEST_LENGTH = 32 +type SHA512_DIGEST_LENGTH = 64 + + +// Recall the 'SHA256State' in our Cryptol model in './SHA256.cry': +/* +type SHA256State = { h : [8][32] + , block : [64][8] + , n : [16] + , sz : [64] + } +*/ + +//////////////////////////////////////////////////////////////// +// Basic hash-state translations. + +// The following code describes how to marshall back and forth between a +// SHA256 C state and a SHA512 C state. Doing this is unnecessary for the +// HMAC verification, but it is necessary to concretely evaluate the specs. +// The rest of this section, therefore, does not need to be trusted. + +// I'm using the initial, high order bits of the SHA512 state to +// construct the SHA256 state. The LLVM code doesn't make it clear +// that this is correct -- it depends on the semantics of 'bitcast' -- +// but I did an experiment which validates this choice; see +// 'examples/llvm/union' in the SAWScript repo. +sha512_c_state_to_sha256_c_state : SHA512_c_state -> SHA256_c_state +sha512_c_state_to_sha256_c_state st = + { h = split (take bits) + , Nl = take (drop`{front=8*32} bits) + , Nh = take (drop`{front=8*32+32} bits) + , u = split (take (drop`{front=8*32+32+32} bits)) + , num = take (drop`{front=8*32+32+32+16*32} bits) + , md_len = drop`{front=8*32+32+32+16*32+32} bits + } + where + bits : [SHA256_c_bits] + bits = take bits0 + bits0 : [SHA512_c_bits] + bits0 = join512_c_state st + +// We need the original state, 'st0', to compute the trailing SHA512 +// bits which aren't used in the SHA256 state. +sha256_c_state_to_sha512_c_state : SHA512_c_state -> SHA256_c_state -> SHA512_c_state +sha256_c_state_to_sha512_c_state st0 st = + { h = split (take bits) + , Nl = take (drop`{front=8*64} bits) + , Nh = take (drop`{front=8*64+64} bits) + , u = split (take (drop`{front=8*64+64+64} bits)) + , num = take (drop`{front=8*64+64+64+16*64} bits) + , md_len = drop`{front=8*64+64+64+16*64+32} bits + } + where + bits : [SHA512_c_bits] + bits = join256_c_state st # drop bits0 + bits0 : [SHA512_c_bits] + bits0 = join512_c_state st0 + +sha256_c_state_to_sha256_state : SHA256_c_state -> SHA256State +sha256_c_state_to_sha256_state st = + { h = st.h + , block = split (join st.u) + , n = drop st.num + , sz = st.Nh # st.Nl + } + where + bits : [SHA256_c_bits] + bits = join256_c_state st + +sha256_state_to_sha256_c_state : SHA256State -> SHA256_c_state +sha256_state_to_sha256_c_state st = + { h = st.h + , Nl = Nl + , Nh = Nh + , u = split (join st.block) + , num = (zero # st.n) : [32] + , md_len = `SHA256_DIGEST_LENGTH : [32] + } + where + [Nh, Nl] = split st.sz + +//////////////////////////////////////////////////////////////// +// Composed hash-state translations. + +sha512_c_state_to_sha256_state : SHA512_c_state -> SHA256State +sha512_c_state_to_sha256_state st = + sha256_c_state_to_sha256_state (sha512_c_state_to_sha256_c_state st) + +sha256_state_to_sha512_c_state : SHA512_c_state -> SHA256State -> SHA512_c_state +sha256_state_to_sha512_c_state st0 st = + sha256_c_state_to_sha512_c_state st0 (sha256_state_to_sha256_c_state st) + +//////////////////////////////////////////////////////////////// +// SHA256 specs in terms of the SHA512 C hash state. + +sha256_init_sha512_c_state : SHA512_c_state -> SHA512_c_state +sha256_init_sha512_c_state st0_c_512 = st1_c_512 + where + st0_256 = SHA256Init + st1_c_512 = sha256_state_to_sha512_c_state st0_c_512 st0_256 + +sha256_update_sha512_c_state : {n} (fin n) => SHA512_c_state -> [n][8] -> SHA512_c_state +sha256_update_sha512_c_state st0_c_512 in = st1_c_512 + where + st0_256 = sha512_c_state_to_sha256_state st0_c_512 + st1_256 = SHA256Update st0_256 in + st1_c_512 = sha256_state_to_sha512_c_state st0_c_512 st1_256 + +// We don't return a new 'SHA512_c_state', since it's unspecified (I +// think ...). +sha256_digest_sha512_c_state : SHA512_c_state -> [SHA256_DIGEST_LENGTH][8] +sha256_digest_sha512_c_state st0_c_512 = out1 + where + st0_256 = sha512_c_state_to_sha256_state st0_c_512 + out1 = split (SHA256Final st0_256) \ No newline at end of file diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.cry b/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.cry new file mode 100644 index 0000000000..e6eaf15d27 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.cry @@ -0,0 +1,193 @@ +/* + * Copyright (c) 2013-2016 Galois, Inc. + * Distributed under the terms of the BSD3 license (see LICENSE file) + * + * @tmd - 24 April 2015 - took Ian's SHA512, converted to SHA256 + * @ian - 15 August 2015 - he lies, probably ment 2014. + * + * This is a very simple implementation of SHA256, designed to be as clearly + * mathced to the specification in NIST's FIPS-PUB-180-4 as possible + * + * * The output correctly matches on all test vectors from + * http://csrc.nist.gov/groups/ST/toolkit/documents/Examples/SHA256.pdf + */ +module SHA256 where + +/* + * SHA256 Functions : Section 4.1.2 + */ + +Ch : [32] -> [32] -> [32] -> [32] +Ch x y z = (x && y) ^ (~x && z) + +Maj : [32] -> [32] -> [32] -> [32] +Maj x y z = (x && y) ^ (x && z) ^ (y && z) + +S0 : [32] -> [32] +S0 x = (x >>> 2) ^ (x >>> 13) ^ (x >>> 22) + +S1 : [32] -> [32] +S1 x = (x >>> 6) ^ (x >>> 11) ^ (x >>> 25) + +s0 : [32] -> [32] +s0 x = (x >>> 7) ^ (x >>> 18) ^ (x >> 3) + +s1 : [32] -> [32] +s1 x = (x >>> 17) ^ (x >>> 19) ^ (x >> 10) + +/* + * SHA256 Constants : Section 4.2.2 + */ + +K : [64][32] +K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5, + 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174, + 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da, + 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967, + 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, + 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070, + 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3, + 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2 + ] + +/* + * Preprocessing (padding and parsing) for SHA256 : Section 5.1.1 and 5.2.1 + */ +preprocess : {msgLen,contentLen,chunks,padding} + ( fin msgLen + , 64 >= width msgLen // message width fits in a word + , contentLen == msgLen + 65 // message + header + , chunks == (contentLen+511) / 512 + , padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0 + ) + => [msgLen] -> [chunks][512] +preprocess msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64])) + +/* + * SHA256 Initial Hash Value : Section 5.3.3 + */ + +H0 : [8][32] +H0 = [ 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, + 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19] + +/* + * The SHA256 Hash computation : Section 6.2.2 + * + * We have split the computation into a message scheduling function, corresponding + * to step 1 in the documents loop, and a compression function, corresponding to steps 2-4. + */ + +SHA256MessageSchedule : [16][32] -> [64][32] +SHA256MessageSchedule M = W where + W = M # [ s1 (W@(j-2)) + (W@(j-7)) + s0 (W@(j-15)) + (W@(j-16)) | j <- [16 .. 63]:[_][8] ] + + + +SHA256Compress : [8][32] -> [64][32] -> [8][32] +SHA256Compress H W = [as!0 + H@0, bs!0 + H@1, cs!0 + H@2, ds!0 + H@3, es!0 + H@4, fs!0 + H@5, gs!0 + H@6, hs!0 + H@7] where + T1 = [h + S1 e + Ch e f g + k + w | h <- hs | e <- es | f <- fs | g <- gs | k <- K | w <- W] + T2 = [S0 a + Maj a b c | a <- as | b <- bs | c <- cs] + hs = take `{65} ([H@7] # gs) + gs = take `{65} ([H@6] # fs) + fs = take `{65} ([H@5] # es) + es = take `{65} ([H@4] # [d + t1 | d <- ds | t1 <- T1]) + ds = take `{65} ([H@3] # cs) + cs = take `{65} ([H@2] # bs) + bs = take `{65} ([H@1] # as) + as = take `{65} ([H@0] # [t1 + t2 | t1 <- T1 | t2 <- T2]) + +SHA256Block : [8][32] -> [16][32] -> [8][32] +SHA256Block H M = SHA256Compress H (SHA256MessageSchedule M) + +//////// Functional/idiomatic top level //////// + +/* + * The SHA256' function hashes a preprocessed sequence of blocks with the + * compression function. The SHA256 function hashes a sequence of bytes, and + * is more likely the function that will be similar to those seein in an + * implementation to be verified. + */ + +SHA256' : {a} (fin a) => [a][16][32] -> [8][32] +SHA256' blocks = hash!0 where + hash = [H0] # [SHA256Block h b | h <- hash | b <- blocks] + +SHA256 : {a} (fin a, 64 >= width (8*a)) => [a][8] -> [256] +SHA256 msg = join (SHA256' [ split x | x <- preprocess(join msg)]) + +property katsPass = ~zero == [test == kat | (test,kat) <- kats ] + +kats = [ (SHA256 "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" + , 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1) + , (SHA256 "" + ,0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855) + , (SHA256 "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu" + , 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1) + // , ([0x61 | i <- [1..1000000] : [_][32]] + // , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0) + ] + +//////// Imperative top level //////// + +type SHA256State = { h : [8][32] + , block : [64][8] + , n : [16] + , sz : [64] + } + +SHA256Init : SHA256State +SHA256Init = { h = H0 + , block = zero + , n = 0 + , sz = 0 + } + +SHA256Update1 : SHA256State -> [8] -> SHA256State +SHA256Update1 s b = + if s.n == 64 + then { h = SHA256Block s.h (split (join s.block)) + , block = [b] # zero + , n = 1 + , sz = s.sz + 8 + } + else { h = s.h + , block = update s.block s.n b + , n = s.n + 1 + , sz = s.sz + 8 + } + +SHA256Update : {n} (fin n) => SHA256State -> [n][8] -> SHA256State +SHA256Update sinit bs = ss!0 + where ss = [sinit] # [ SHA256Update1 s b | s <- ss | b <- bs ] + +// Add padding and size and process the final block. +SHA256Final : SHA256State -> [256] +SHA256Final s = join (SHA256Block h b') + // Because the message is always made up of bytes, and the size is a + // fixed number of bytes, the 1 pad will always be at least a byte. + where s' = SHA256Update1 s 0x80 + // Don't need to add zeros. They're already there. Just update + // the count of bytes in this block. After adding the 1 pad, there + // are two possible cases: the size will fit in the current block, + // or it won't. + (h, b) = if s'.n <= 56 then (s'.h, s'.block) + else (SHA256Block s'.h (split (join s'.block)), zero) + b' = split (join b || (zero # s.sz)) + +SHA256Imp : {a} (64 >= width (8*a)) => [a][8] -> [256] +SHA256Imp msg = SHA256Final (SHA256Update SHA256Init msg) + +property katsPassImp = ~zero == [test == kat | (test,kat) <- katsImp ] + +katsImp = [ (SHA256Imp "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" + , 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1) + , (SHA256Imp "" + , 0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855) + , (SHA256Imp "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu" + , 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1) + // , ([0x61 | i <- [1..1000000] : [_][32]] + // , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0) + ] + +property imp_correct msg = SHA256 msg == SHA256Imp msg diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.py b/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.py new file mode 100644 index 0000000000..77686db53d --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.py @@ -0,0 +1,20 @@ +# TODO (now) + +# SHA256.saw +# import "SHA256.cry"; + +# let check_sha n = do { +# print (str_concat "Checking imp_correct for byte count " (show n)); +# time (prove_print abc {{ imp_correct : [n][8] -> Bit }}); +# }; + +# for [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] check_sha; +# for [17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32] check_sha; +# for [33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48] check_sha; +# for [49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64] check_sha; +# for [65, 127, 128, 129, 1000] check_sha; + + + + + diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.saw b/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.saw new file mode 100644 index 0000000000..f7348a3977 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/SHA256.saw @@ -0,0 +1,33 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +import "SHA256.cry"; + +let check_sha n = do { + print (str_concat "Checking imp_correct for byte count " (show n)); + time (prove_print abc {{ imp_correct : [n][8] -> Bit }}); +}; + +for [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] check_sha; +for [17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32] check_sha; +for [33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48] check_sha; +for [49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64] check_sha; +for [65, 127, 128, 129, 1000] check_sha; diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/modthm.cry b/saw-remote-api/test-scripts/in-progress/HMAC/spec/modthm.cry new file mode 100644 index 0000000000..6ef16df2a2 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/modthm.cry @@ -0,0 +1,21 @@ +valid_block_sizes : [16] -> [16] -> Bit +valid_block_sizes hbs bs = + // We're not handling SSLv3 yet. + //((bs, hbs) == (40, 64)) || + //((bs, hbs) == (48, 64)) || + ((bs, hbs) == (64, 64)) || + ((bs, hbs) == (128, 128)) + +modthm : [32] -> [32] -> [32] -> [16] -> [16] -> Bit +modthm x11 x15 x16 hash_block_size block_size = + ((((x11 + (x16 % x17)) % x18) + (x15 % x17)) % x18) + == + ((x11 + ((x16 + x15) % x17)) % x18) + where x17 = zero # hash_block_size + x18 = zero # block_size + +modthm_precond : [32] -> [32] -> [32] -> [16] -> [16] -> Bit +modthm_precond x11 x15 x16 hash_block_size block_size = + if (valid_block_sizes hash_block_size block_size) then + modthm x11 x15 x16 hash_block_size block_size + else True diff --git a/saw-remote-api/test-scripts/in-progress/drbg/drbg-helpers.cry b/saw-remote-api/test-scripts/in-progress/drbg/drbg-helpers.cry new file mode 100644 index 0000000000..06b60a7a51 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/drbg/drbg-helpers.cry @@ -0,0 +1,44 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2019 Galois, Inc. All Rights Reserved +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//import Primitive::Keyless::Generator::DRBG +import DRBG +import AES + +// TODO: the original version of this, keysize = 32 conflicted +// in the definition of encrypt_128 +type keysize = 16 // keylen / 8 + +max_seq_number : [blocksize*8] +max_seq_number = ~zero + +drbg_generate_seedlen : s2n_drbg -> [seedlen] -> Bit -> ([seedlen], s2n_drbg) +drbg_generate_seedlen = drbg_generate `{n=seedlen,blocks=2} + +encrypt_128 : [keysize][8] -> [blocksize][8] -> [blocksize][8] +encrypt_128 key msg = + split (block_encrypt (join key) (join msg)) + +mode_128 = 0 +mode_256 = 1 + +// TODO: Tried to simulate the top-level symbolic variable from the +// saw script version using undefined below, but in the end +// this trick did not work. +// Note: I changed this. Originally it was seedsize, but +// that appears to be 48 here which prevents some proofs +// from going through. +//type entropy_len = 32 +//fake_entropy : [entropy_len*8] +//fake_entropy = undefined diff --git a/saw-remote-api/test-scripts/in-progress/drbg/drbg.py b/saw-remote-api/test-scripts/in-progress/drbg/drbg.py new file mode 100755 index 0000000000..a97cbe4465 --- /dev/null +++ b/saw-remote-api/test-scripts/in-progress/drbg/drbg.py @@ -0,0 +1,325 @@ +#!/usr/bin/env python3 +import os +import os.path +from saw import * +from saw.llvm import Contract +from saw.proofscript import yices +from cryptol import cry, cryptoltypes +#from saw.dashboard import Dashboard + +dir_path = os.path.dirname(os.path.realpath(__file__)) +conn = connect("cabal -v0 run exe:saw-remote-api socket") +view(DebugLog(err=None)) +view(LogResults()) +#view(Dashboard(path=__file__)) + +bcname = os.path.join(dir_path, '../all_llvm.bc') +cryname = '/home/dagit/local-data/saw/s2n/tests/saw/spec/DRBG/DRBG.cry' +drbghelpers = '/home/dagit/local-data/saw/saw-script/drbg-helpers.cry' + +cryptol_load_file(cryname) +cryptol_load_file(drbghelpers) + +mod = llvm_load_module(bcname) + +def bytes_type(size): + return llvm_types.array(size, llvm_types.i8) + +blocksize = 16 # blocklen / 8 +keysize = 16 # keylen / 8 +seedsize = 32 + +blob_type = llvm_types.alias('struct.s2n_blob') +ctx_type = bytes_type(keysize) + +def alloc_bytes(spec, n): + return spec.alloc(bytes_type(n)) + +def alloc_blob(spec, n): + p = spec.alloc(type=blob_type, read_only=True) + datap = alloc_bytes(spec, n) + spec.points_to(llvm.field(p, "data"), datap) + spec.points_to(llvm.field(p, "size"), llvm.cryptol("`{n}:[32]".format(n=n))) + spec.points_to(llvm.field(p, "allocated"), llvm.cryptol("0:[32]")) + spec.points_to(llvm.field(p, "growable"), llvm.cryptol("0:[8]")) + return (p, datap) + +def alloc_blob_readonly(spec, n): + p = spec.alloc(type=blob_type, read_only=True) + datap = spec.alloc(llvm_types.array(n, llvm_types.i8), read_only = True) + spec.points_to(llvm.field(p, "data"), datap) + spec.points_to(llvm.field(p, "size"), llvm.cryptol("`{n}: [32]".format(n=n))) + return(p, datap) + +def alloc_init(spec, ty, v): + p = spec.alloc(ty) + spec.points_to(p,v) + return p + +def alloc_init_readonly(spec, ty, v): + p = spec.alloc(ty, read_only = True) + spec.points_to(p, v) + return p + +def ptr_to_fresh(spec, n, ty): + x = spec.fresh_var(ty, n) + p = alloc_init(spec, ty, x) + return (x, p) + +def fresh_ptr(spec, ty): + x = spec.fresh_var(ty) + p = spec.alloc(ty, points_to = x) + return p + +def ptr_to_fresh_readonly(spec, n, ty): + x = spec.fresh_var(ty, n); + p = alloc_init_readonly(spec, ty, x) + return (x, p) + +def drbg_state(spec, n): + state = spec.alloc(llvm_types.alias("struct.s2n_drbg")) + (key, keyp) = ptr_to_fresh(spec, "key", ctx_type) + bytes_used = spec.fresh_var(llvm_types.i64, n+"bytes_used") + mixes = spec.fresh_var(llvm_types.i64, n+"mixes") + v = spec.fresh_var(bytes_type(blocksize), n+"v") + spec.points_to(llvm.field(state, "bytes_used"), bytes_used) + spec.points_to(llvm.field(state, "mixes"), mixes) + spec.points_to(llvm.field(state, "ctx"), keyp) + spec.points_to(llvm.field(state, "v"), v) + return (state, keyp, + "{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}".format(bytes_used=bytes_used.name(), key=key.name(), v=v.name())) + #return (state, keyp, + # llvm.cryptol("{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}".format(bytes_used=bytes_used.name(), key=key.name(), v=v.name()))) + #return (state, keyp, { 'bytes_used': bytes_used , 'ctx': { 'key': llvm.cryptol("join {}".format(key.name())) } , v: llvm.cryptol("join {}".format(v)) }) + + # , {{ { bytes_used = bytes_used + # , ctx = { key = join key } + # , v = join v + # } }} + +class blob_zero_spec(Contract): + def __init__(self,n): + super().__init__() + self.n = n + + def specification(self): + (p, datap) = alloc_blob(self, self.n) + self.execute_func(p) + self.points_to(datap, llvm.cryptol("zero:[{n}][8]".format(n=self.n))) + self.returns(llvm.cryptol("0:[32]")) + +class increment_drbg_counter_spec(Contract): + def specification(self): + (p, datap) = alloc_blob(self, blocksize) + v = self.fresh_var(bytes_type(blocksize), "v") + self.points_to(datap, v) + self.execute_func(p) + self.points_to(datap, llvm.cryptol("split ((join {v}) +1): [{blocksize}][8]".format(v=v.name(),blocksize=blocksize))) + self.returns(llvm.cryptol("0:[32]")) + +class bytes_used_spec(Contract): + def specification(self): + (sp, keyp, s) = drbg_state(self,"drbg") + bytes_used = alloc_init(self, llvm_types.i64, llvm.cryptol("0:[64]")) + self.execute_func(sp, bytes_used) + self.points_to(bytes_used, llvm.cryptol("{s}.bytes_used".format(s=s))) + self.returns(llvm.cryptol("0:[32]")) + +class block_encrypt_spec(Contract): + def specification(self): + (key, keyp) = ptr_to_fresh_readonly(self, "ctx", ctx_type) + (msg, msgp) = ptr_to_fresh_readonly(self, "msg", bytes_type(blocksize)) + outp = alloc_bytes(self, blocksize) + self.execute_func(keyp, msgp, outp) + self.points_to(outp, llvm.cryptol("encrypt_128 {key} {msg}".format(key=key.name(), msg=msg.name()))) + self.returns(llvm.cryptol("0 : [32]")) + +class encryptUpdate_spec(Contract): + def __init__(self,n): + super().__init__() + self.n = n + def specification(self): + # the first argument of `EVP_EncryptUpdate` is not `const`, + # but it is constant in the DRBG cryptol specification. + (key, keyp) = ptr_to_fresh_readonly(self, "key", ctx_type) + outp = alloc_bytes(self, self.n) + lenp = alloc_init(self, llvm_types.i32, llvm.cryptol("{} : [32]".format(self.n))) + (msg, msgp) = ptr_to_fresh_readonly(self, "msg", (bytes_type(self.n))) + self.execute_func(keyp, outp, lenp, msgp, llvm.cryptol("`{blocksize} : [32]".format(blocksize=blocksize))) + self.points_to(outp, llvm.cryptol("encrypt_128 {} {}".format(key.name(), msg.name()))) + self.points_to(lenp, llvm.cryptol("{} : [32]".format(self.n))) + self.returns (llvm.cryptol("1 : [32]")) + +class bits_spec(Contract): + def __init__(self, n): + super().__init__() + self.n = n + def specification(self): + (sp, keyp, s) = drbg_state(self, "drbg") + (outp, datap) = alloc_blob(self, self.n) + self.execute_func(sp, outp) + res = "drbg_generate_internal `{{n={n}*8}} ({s})".format(n=self.n,s=s) + # Remove some of the parens here to get really bad error messages + c = llvm.cryptol("split (({res}).0) : [{n}][8]".format(res=res, n=self.n)) + self.points_to(datap, c) + ensure_drbg_state(self, sp, keyp, "({res}).1".format(res=res)) + self.returns (llvm.cryptol(" 0 : [32] ")) + +def ensure_drbg_state(spec, p, keyp, s): + spec.points_to(llvm.field(p, "bytes_used"), llvm.cryptol("({s}).bytes_used".format(s=s))) + spec.points_to(llvm.field(p, "ctx"), keyp) + spec.points_to(keyp, llvm.cryptol("split (({s}).ctx.key) : [{keysize}][8]".format(s=s,keysize=keysize))) + spec.points_to(llvm.field(p, "v"), llvm.cryptol("split (({s}).v) : [{blocksize}][8]".format(s=s,blocksize=blocksize))) + mixes = spec.fresh_var(llvm_types.i64, "mixes") + spec.points_to(llvm.field(p, "mixes"), mixes) + +#//////////////////////////////////////////////////////////////////////////////// +#// Assumed specifications +#//////////////////////////////////////////////////////////////////////////////// + +class getenv_spec(Contract): + def specification(self): + p = self.alloc(llvm_types.i8) + self.execute_func(p) + self.returns(llvm.null) + +class aes_128_ecb_spec(Contract): + def specification(self): + self.execute_func() + r = self.alloc(ctx_type) + self.returns(r) + +class cipher_new_spec(Contract): + def specification(self): + self.execute_func() + r = self.alloc(ctx_type) + self.returns(r) + +class cipher_init_spec(Contract): + def specification(self): + ctx = self.alloc(ctx_type) + self.execute_func(ctx) + key = self.fresh_var(ctx_type, "key") + self.points_to(ctx, key) + +class cipher_free_spec(Contract): + def specification(self): + ctx = self.alloc(ctx_type) + self.execute_func(ctx) + self.returns(llvm.void) + +class cipher_cleanup_spec(Contract): + def specification(self): + ctx = self.alloc(ctx_type) + self.execute_func(ctx) + self.points_to(ctx, llvm.cryptol("zero : [{keysize}][8]".format(keysize=keysize))) + self.returns(llvm.cryptol("1:[32]")) + +class cipher_key_length_spec(Contract): + def specification(self): + ctx = self.alloc(ctx_type, read_only = True) + self.execute_func(ctx) + # Specialized to AES-128 for now + self.returns(llvm.cryptol("16:[32]")) + +class encryptInit_spec(Contract): + def specification(self): + ctx = self.alloc(ctx_type) + #(ct, ctx) = ptr_to_fresh(self, "ctx", ctx_type) + #(st, stp) = ptr_to_fresh(self, "st", ctx_type) + #st = self.fresh_var(ctx_type) + #stp = self.alloc(ctx_type, points_to = st) + (key, keyp) = ptr_to_fresh_readonly(self, "key", ctx_type) + #self.execute_func(ctx, stp, llvm.null, keyp, llvm.null) + self.execute_func(ctx, llvm.null, llvm.null, keyp, llvm.null) + self.points_to(ctx, key) + self.returns(llvm.cryptol("1:[32]")) + +class get_public_random_spec(Contract): + def __init__(self): + super().__init__() + + def specification(self): + (p, datap) = alloc_blob(self, seedsize) + self.execute_func(p) + # TODO: blocked on 'fake_entropy' + #self.points_to(datap, llvm.cryptol("split fake_entropy : [{seedsize}][8]".format(seedsize=seedsize))) + self.returns(llvm.cryptol("0: [32]")) + +class supports_rdrand_spec(Contract): + def specification(self): + self.execute_func() + r = self.fresh_var(llvm_types.i8, "supports_rdrand") + self.returns(r) + +#//////////////////////////////////////////////////////////////////////////////// +#// Assumptions about external functions +#//////////////////////////////////////////////////////////////////////////////// + +getenv_ov = llvm_assume(mod, "getenv", getenv_spec()) +aes_128_ecb_ov = llvm_assume(mod, "EVP_aes_128_ecb", aes_128_ecb_spec()) +cipher_new_ov = llvm_assume(mod, "EVP_CIPHER_CTX_new", cipher_new_spec()) +cipher_free_ov = llvm_assume(mod, "EVP_CIPHER_CTX_free", cipher_free_spec()) +#cipher_cleanup_ov = llvm_assume(mod, "EVP_CIPHER_CTX_reset", cipher_cleanup_spec()) +cipher_key_length_ov = llvm_assume(mod, "EVP_CIPHER_CTX_key_length", cipher_key_length_spec()) +encryptInit_ov = llvm_assume(mod, "EVP_EncryptInit_ex", encryptInit_spec()) +#encryptInit_nokey_ov = llvm_assume(mod, "EVP_EncryptInit_ex", encryptInit_nokey_spec()) +encryptUpdate_ov = llvm_assume(mod, "EVP_EncryptUpdate", encryptUpdate_spec(16)) +supports_rdrand_ov = llvm_assume(mod, "s2n_cpu_supports_rdrand", supports_rdrand_spec()) +# TODO: blocked on 'fake_entropy' +#get_public_random_ov = llvm_assume(mod, "s2n_get_public_random_data", get_public_random_spec()) +get_seed_entropy_ov = llvm_assume(mod, "s2n_get_seed_entropy", get_public_random_spec()) +get_mix_entropy_ov = llvm_assume(mod, "s2n_get_mix_entropy", get_public_random_spec()) + +### +class update_spec(Contract): + def __init__(self, n): + super().__init__() + self.n = n + def specification(self): + (sp, keyp, s) = drbg_state(self, "drbg") + (providedp, datap) = alloc_blob_readonly(self, self.n) + data = self.fresh_var(bytes_type(self.n), "data") + self.points_to(datap, data) + self.execute_func(sp, providedp) + ensure_drbg_state(self, sp, keyp, "drbg_update (join {data}) ({s})".format(data=data.name(), s=s)) + self.returns(llvm.cryptol("0:[32]")) + +class seed_spec(Contract): + def __init__(self, n): + super().__init__() + self.n = n + def specification(self): + (sp, keyp, s) = drbg_state(self, "drbg") + (psp, datap) = alloc_blob_readonly(self, self.n) + data = self.fresh_var(bytes_type(self.n), "data") + self.points_to(datap, data) + self.execute_func(sp, psp) + expr = "drbg_reseed ({s}) (fake_entropy) (join ({data}))".format(s=s, + data=data.name()) + ensure_drbg_state(self, sp, keyp, expr) + self.returns(llvm.cryptol("0:[32]")) + +zero_ov_block = llvm_verify(mod, 's2n_blob_zero', blob_zero_spec(blocksize)) +zero_ov_seed = llvm_verify(mod, "s2n_blob_zero", blob_zero_spec(seedsize)) +zero_ov_drbg = llvm_verify(mod, "s2n_blob_zero", blob_zero_spec(48)) + +inc_ov = llvm_verify(mod, "s2n_increment_drbg_counter", increment_drbg_counter_spec()) +llvm_verify(mod, "s2n_drbg_bytes_used", bytes_used_spec()) + + +blk_enc_ov = llvm_verify(mod, "s2n_drbg_block_encrypt", contract = block_encrypt_spec(), lemmas = [encryptUpdate_ov], script = yices(unints=['block_encrypt'])) + +bits_ov = llvm_verify(mod, "s2n_drbg_bits", contract = bits_spec(seedsize), + lemmas = [inc_ov, encryptUpdate_ov, blk_enc_ov], script = yices(['block_encrypt'])) + +update_ov = llvm_verify(mod, "s2n_drbg_update", lemmas = [bits_ov, + encryptInit_ov, aes_128_ecb_ov, cipher_key_length_ov], contract= + update_spec(seedsize), script = yices(["block_encrypt"])) + +# TODO: this lemma cannot be proven yet, see drbg-helpers.cry for the definition +# of "fake_entropy" +#seed_ov = llvm_verify(mod, "s3n_drbg_seed", lemmas = [get_public_random_ov, +# get_seed_entropy_ov, update_ov, cipher_key_length_ov], contract = +# seed_spec(seedsize), +# script = yices(["block_encrypt"])) diff --git a/saw-remote-api/test-scripts/llvm_struct.bc b/saw-remote-api/test-scripts/llvm_struct.bc new file mode 100644 index 0000000000..7675ba4d12 Binary files /dev/null and b/saw-remote-api/test-scripts/llvm_struct.bc differ diff --git a/saw-remote-api/test-scripts/llvm_struct.c b/saw-remote-api/test-scripts/llvm_struct.c new file mode 100644 index 0000000000..720155d9db --- /dev/null +++ b/saw-remote-api/test-scripts/llvm_struct.c @@ -0,0 +1,16 @@ +typedef struct { + unsigned int *x; +} s; + +int add_indirect(s *o) { + return (o->x)[0] + (o->x)[1]; +} + +void set_indirect(s *o) { + (o->x)[0] = 0; + (o->x)[1] = 0; +} + +s *s_id(s *o) { + return o; +} diff --git a/saw-remote-api/test-scripts/llvm_struct.py b/saw-remote-api/test-scripts/llvm_struct.py new file mode 100644 index 0000000000..2894ebc574 --- /dev/null +++ b/saw-remote-api/test-scripts/llvm_struct.py @@ -0,0 +1,78 @@ +import os +import os.path +from cryptol.cryptoltypes import to_cryptol +from saw import * +from saw.llvm import Contract, SetupVal, FreshVar, cryptol, struct, LLVMType, void +import saw.llvm_types as ty +from env_server import * + + +def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]: + """Add to``Contract`` ``c`` an allocation of a pointer of type ``ty`` initialized to an unknown fresh value. + + :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh + variable will be assigned ``name`` if provided/available.)""" + var = c.fresh_var(ty, name) + ptr = c.alloc(ty, points_to = var) + return (var, ptr) + +# let set_spec = do { +# (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32)); +# po <- alloc_init (llvm_struct "struct.s") (crucible_struct [px]); +# crucible_execute_func [po]; +# crucible_points_to po (crucible_struct [px]); +# crucible_points_to px (crucible_term {{ [0, 0] : [2][32] }}); +# }; +class SetContract(Contract): + def specification(self): + (_, x_p) = ptr_to_fresh(self, ty.array(2, ty.i32), "x") + p = self.alloc(ty.alias('struct.s'), points_to=struct(x_p)) + + self.execute_func(p) + + self.points_to(p, struct(x_p)) + self.points_to(x_p, cryptol('[0, 0] : [2][32]')) + self.returns(void) + +# let add_spec = do { +# (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32)); +# po <- alloc_init (llvm_struct "struct.s") (crucible_struct [px]); +# crucible_execute_func [po]; +# crucible_return (crucible_term {{ x@0 + x@1 }}); +# }; +class AddContract(Contract): + def specification(self): + (x, x_p) = ptr_to_fresh(self, ty.array(2, ty.i32), "x") + p = self.alloc(ty.alias('struct.s'), points_to=struct(x_p)) + + self.execute_func(p) + + self.returns(cryptol(f'{x.name()}@0 + {x.name()}@1')) + +# let id_spec = do { +# (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32)); +# po <- alloc_init (llvm_struct "struct.s") (crucible_struct [px]); +# crucible_execute_func [po]; +# crucible_return po; +# }; +class IdContract(Contract): + def specification(self): + (x, x_p) = ptr_to_fresh(self, ty.array(2, ty.i32), "x") + p = self.alloc(ty.alias('struct.s'), points_to=struct(x_p)) + + self.execute_func(p) + + self.returns(p) + +dir_path = os.path.dirname(os.path.realpath(__file__)) +env_connect_global() +view(LogResults()) +bcname = os.path.join(dir_path, 'llvm_struct.bc') +mod = llvm_load_module(bcname) + +# crucible_llvm_verify m "set_indirect" [] false set_spec abc; +result = llvm_verify(mod, 'set_indirect', SetContract()) +# crucible_llvm_verify m "add_indirect" [] false add_spec abc; +result = llvm_verify(mod, 'add_indirect', AddContract()) +# crucible_llvm_verify m "s_id" [] false id_spec abc; +result = llvm_verify(mod, 's_id', IdContract()) diff --git a/saw-remote-api/test-scripts/salsa20.py b/saw-remote-api/test-scripts/salsa20.py index d01ddcaf9d..b55b33977f 100755 --- a/saw-remote-api/test-scripts/salsa20.py +++ b/saw-remote-api/test-scripts/salsa20.py @@ -3,6 +3,7 @@ import os.path import saw.connection as saw from saw.llvm import * +from saw.llvm_types import i8, i32, LLVMArrayType from saw.proofscript import * from env_server import * @@ -25,10 +26,10 @@ shift = {"setup value": "Cryptol", "expression": "shift" } res = {"setup value": "Cryptol", "expression": "value <<< shift" } -y0p = {"setup value": "saved", "name" : "y0p" } -y1p = {"setup value": "saved", "name" : "y1p" } -y2p = {"setup value": "saved", "name" : "y2p" } -y3p = {"setup value": "saved", "name" : "y3p" } +y0p = {"setup value": "named", "name" : "y0p" } +y1p = {"setup value": "named", "name" : "y1p" } +y2p = {"setup value": "named", "name" : "y2p" } +y3p = {"setup value": "named", "name" : "y3p" } y0 = {"setup value": "Cryptol", "expression" : "y0" } y1 = {"setup value": "Cryptol", "expression" : "y1" } @@ -40,7 +41,7 @@ y2f = {"setup value": "Cryptol", "expression" : "(quarterround [y0, y1, y2, y3]) @ 2" } y3f = {"setup value": "Cryptol", "expression" : "(quarterround [y0, y1, y2, y3]) @ 3" } -yp = {"setup value": "saved", "name" : "yp" } +yp = {"setup value": "named", "name" : "yp" } y = {"setup value": "Cryptol", "expression" : "y" } rr_res = {"setup value": "Cryptol", "expression" : "rowround y" } @@ -52,8 +53,8 @@ rotl_contract = { "pre vars": [ - {"server name": "value", "name": "value", "type": uint32_t.to_json()}, - {"server name": "shift", "name": "shift", "type": uint32_t.to_json()} + {"server name": "value", "name": "value", "type": i32.to_json()}, + {"server name": "shift", "name": "shift", "type": i32.to_json()} ], "pre conds": ["0 < shift /\\ shift < 32"], "pre allocated": [], @@ -68,27 +69,27 @@ qr_contract = { "pre vars": [ - {"server name": "y0", "name": "y0", "type": uint32_t.to_json()}, - {"server name": "y1", "name": "y1", "type": uint32_t.to_json()}, - {"server name": "y2", "name": "y2", "type": uint32_t.to_json()}, - {"server name": "y3", "name": "y3", "type": uint32_t.to_json()} + {"server name": "y0", "name": "y0", "type": i32.to_json()}, + {"server name": "y1", "name": "y1", "type": i32.to_json()}, + {"server name": "y2", "name": "y2", "type": i32.to_json()}, + {"server name": "y3", "name": "y3", "type": i32.to_json()} ], "pre conds": [], "pre allocated": [ {"server name": "y0p", - "type": uint32_t.to_json(), + "type": i32.to_json(), "mutable": True, "alignment": None}, {"server name": "y1p", - "type": uint32_t.to_json(), + "type": i32.to_json(), "mutable": True, "alignment": None}, {"server name": "y2p", - "type": uint32_t.to_json(), + "type": i32.to_json(), "mutable": True, "alignment": None}, {"server name": "y3p", - "type": uint32_t.to_json(), + "type": i32.to_json(), "mutable": True, "alignment": None} ], @@ -128,35 +129,35 @@ def oneptr_update_contract(ty, res): "return val": None } -rr_contract = oneptr_update_contract(LLVMArrayType(uint32_t, 16), rr_res) -cr_contract = oneptr_update_contract(LLVMArrayType(uint32_t, 16), cr_res) -dr_contract = oneptr_update_contract(LLVMArrayType(uint32_t, 16), dr_res) -hash_contract = oneptr_update_contract(LLVMArrayType(uint8_t, 64), hash_res) +rr_contract = oneptr_update_contract(LLVMArrayType(i32, 16), rr_res) +cr_contract = oneptr_update_contract(LLVMArrayType(i32, 16), cr_res) +dr_contract = oneptr_update_contract(LLVMArrayType(i32, 16), dr_res) +hash_contract = oneptr_update_contract(LLVMArrayType(i8, 64), hash_res) -kp = {"setup value": "saved", "name" : "kp" } -np = {"setup value": "saved", "name" : "np" } -ksp = {"setup value": "saved", "name" : "ksp" } +kp = {"setup value": "named", "name" : "kp" } +np = {"setup value": "named", "name" : "np" } +ksp = {"setup value": "named", "name" : "ksp" } k = {"setup value": "Cryptol", "expression" : "k" } n = {"setup value": "Cryptol", "expression" : "n" } zero = {"setup value": "Cryptol", "expression" : "0 : [32]" } expand_contract = { "pre vars": [ - {"server name": "k", "name": "k", "type": LLVMArrayType(uint8_t, 32).to_json()}, - {"server name": "n", "name": "n", "type": LLVMArrayType(uint8_t, 16).to_json()} + {"server name": "k", "name": "k", "type": LLVMArrayType(i8, 32).to_json()}, + {"server name": "n", "name": "n", "type": LLVMArrayType(i8, 16).to_json()} ], "pre conds": [], "pre allocated": [ {"server name": "kp", - "type": LLVMArrayType(uint8_t, 32).to_json(), + "type": LLVMArrayType(i8, 32).to_json(), "mutable": True, "alignment": None}, {"server name": "np", - "type": LLVMArrayType(uint8_t, 16).to_json(), + "type": LLVMArrayType(i8, 16).to_json(), "mutable": True, "alignment": None}, {"server name": "ksp", - "type": LLVMArrayType(uint8_t, 64).to_json(), + "type": LLVMArrayType(i8, 64).to_json(), "mutable": True, "alignment": None} ], @@ -170,29 +171,29 @@ def oneptr_update_contract(ty, res): "return val": None } -vp = {"setup value": "saved", "name" : "vp" } -mp = {"setup value": "saved", "name" : "mp" } +vp = {"setup value": "named", "name" : "vp" } +mp = {"setup value": "named", "name" : "mp" } v = {"setup value": "Cryptol", "expression" : "v" } m = {"setup value": "Cryptol", "expression" : "m" } def crypt_contract(size : int): return { "pre vars": [ - {"server name": "k", "name": "k", "type": LLVMArrayType(uint8_t, 32).to_json()}, - {"server name": "v", "name": "v", "type": LLVMArrayType(uint8_t, 8).to_json()}, - {"server name": "m", "name": "m", "type": LLVMArrayType(uint8_t, size).to_json()} + {"server name": "k", "name": "k", "type": LLVMArrayType(i8, 32).to_json()}, + {"server name": "v", "name": "v", "type": LLVMArrayType(i8, 8).to_json()}, + {"server name": "m", "name": "m", "type": LLVMArrayType(i8, size).to_json()} ], "pre conds": [], "pre allocated": [ {"server name": "kp", - "type": LLVMArrayType(uint8_t, 32).to_json(), + "type": LLVMArrayType(i8, 32).to_json(), "mutable": True, "alignment": None}, {"server name": "vp", - "type": LLVMArrayType(uint8_t, 8).to_json(), + "type": LLVMArrayType(i8, 8).to_json(), "mutable": True, "alignment": None}, {"server name": "mp", - "type": LLVMArrayType(uint8_t, size).to_json(), + "type": LLVMArrayType(i8, size).to_json(), "mutable": True, "alignment": None} ], diff --git a/saw-remote-api/test-scripts/salsa20_easy.py b/saw-remote-api/test-scripts/salsa20_easy.py index 6b2d807b4e..e52eb69d15 100644 --- a/saw-remote-api/test-scripts/salsa20_easy.py +++ b/saw-remote-api/test-scripts/salsa20_easy.py @@ -2,7 +2,8 @@ import os.path from cryptol.cryptoltypes import to_cryptol from saw import * -from saw.llvm import Contract, LLVMArrayType, uint8_t, uint32_t, void +from saw.llvm import Contract, void, SetupVal, FreshVar, cryptol +from saw.llvm_types import i8, i32, LLVMType, LLVMArrayType from env_server import * dir_path = os.path.dirname(os.path.realpath(__file__)) @@ -17,143 +18,110 @@ mod = llvm_load_module(bcname) -class RotlContract(Contract): - def pre(self): - self.value = self.declare(uint32_t) - self.shift = self.declare(uint32_t) - self.proclaim(self.shift > self.cryptol("0")) - self.proclaim(self.shift < self.cryptol("32")) - def call(self): - self.arguments(self.value, self.shift) - def post(self): - self.returns(self.cryptol("(<<<)")(self.value, self.shift)) - +def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]: + """Add to``Contract`` ``c`` an allocation of a pointer of type ``ty`` initialized to an unknown fresh value. + + :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh + variable will be assigned ``name`` if provided/available.)""" + var = c.fresh_var(ty, name) + ptr = c.alloc(ty, points_to = var) + return (var, ptr) -rotl_result = llvm_verify(mod, 'rotl', RotlContract()) +def oneptr_update_func(c : Contract, ty : LLVMType, fn_name : str) -> None: + """Upcates contract ``c`` to declare calling it with a pointer of type ``ty`` + updates that pointer with the result, which is equal to calling the + Cryptol function ``fn_name``.""" + (x, x_p) = ptr_to_fresh(c, ty) -class TrivialContract(Contract): - def post(self): self.returns(void) + c.execute_func(x_p) -class QuarterRoundContract(Contract): - def pre(self): - self.y0 = self.declare(uint32_t) - self.y1 = self.declare(uint32_t) - self.y2 = self.declare(uint32_t) - self.y3 = self.declare(uint32_t) - - self.y0_p = self.declare_pointer(uint32_t) - self.y1_p = self.declare_pointer(uint32_t) - self.y2_p = self.declare_pointer(uint32_t) - self.y3_p = self.declare_pointer(uint32_t) - - self.points_to(self.y0_p, self.y0) - self.points_to(self.y1_p, self.y1) - self.points_to(self.y2_p, self.y2) - self.points_to(self.y3_p, self.y3) - - def call(self): - self.arguments(self.y0_p, self.y1_p, self.y2_p, self.y3_p) - - def post(self): - self.points_to(self.y0_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("0"))) - self.points_to(self.y1_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("1"))) - self.points_to(self.y2_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("2"))) - self.points_to(self.y3_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("3"))) - self.returns(void) + c.points_to(x_p, cryptol(fn_name)(x)) + c.returns(void) + return None -qr_result = llvm_verify(mod, 's20_quarterround', QuarterRoundContract(), lemmas=[rotl_result]) - - -class OnePointerUpdateContract(Contract): - def __init__(self, the_type): - super().__init__() - self.t = the_type +class RotlContract(Contract): + def specification(self) -> None: + value = self.fresh_var(i32, "value") + shift = self.fresh_var(i32, "shift") + self.proclaim(shift > cryptol("0")) + self.proclaim(shift < cryptol("32")) + self.execute_func(value, shift) - def pre(self): - self.y = self.declare(self.t) - self.y_p = self.declare_pointer(self.t) - self.points_to(self.y_p, self.y) + self.returns(cryptol("(<<<)")(value, shift)) - def call(self): - self.arguments(self.y_p) - def post(self): +rotl_result = llvm_verify(mod, 'rotl', RotlContract()) +class QuarterRoundContract(Contract): + def specification(self) -> None: + y0 = self.fresh_var(i32, "y0") + y1 = self.fresh_var(i32, "y1") + y2 = self.fresh_var(i32, "y2") + y3 = self.fresh_var(i32, "y3") + + y0_p = self.alloc(i32, points_to=y0) + y1_p = self.alloc(i32, points_to=y1) + y2_p = self.alloc(i32, points_to=y2) + y3_p = self.alloc(i32, points_to=y3) + + self.execute_func(y0_p, y1_p, y2_p, y3_p) + + res = cryptol("quarterround")([y0, y1, y2, y3]) + self.points_to(y0_p, cryptol("(@)")(res, cryptol("0"))) + self.points_to(y1_p, cryptol("(@)")(res, cryptol("1"))) + self.points_to(y2_p, cryptol("(@)")(res, cryptol("2"))) + self.points_to(y3_p, cryptol("(@)")(res, cryptol("3"))) self.returns(void) -class RowRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) +qr_result = llvm_verify(mod, 's20_quarterround', QuarterRoundContract(), lemmas=[rotl_result]) - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("rowround")(self.y)) -rr_result = llvm_verify(mod, 's20_rowround', RowRoundContract(), lemmas=[qr_result]) +class RowRoundContract(Contract): + def specification(self) -> None: + oneptr_update_func(self, LLVMArrayType(i32, 16), "rowround") +rr_result = llvm_verify(mod, 's20_rowround', RowRoundContract(), lemmas=[qr_result]) -class ColumnRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("columnround")(self.y)) +class ColumnRoundContract(Contract): + def specification(self) -> None: + oneptr_update_func(self, LLVMArrayType(i32, 16), "columnround") cr_result = llvm_verify(mod, 's20_columnround', ColumnRoundContract(), lemmas=[rr_result]) -class DoubleRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("doubleround")(self.y)) +class DoubleRoundContract(Contract): + def specification(self) -> None: + oneptr_update_func(self, LLVMArrayType(i32, 16), "doubleround") dr_result = llvm_verify(mod, 's20_doubleround', DoubleRoundContract(), lemmas=[cr_result, rr_result]) -class HashContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint8_t, 64)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("Salsa20")(self.y)) +class HashContract(Contract): + def specification(self) -> None: + oneptr_update_func(self, LLVMArrayType(i8, 64), "Salsa20") hash_result = llvm_verify(mod, 's20_hash', HashContract(), lemmas=[dr_result]) -class ExpandContract(Contract): - def pre(self): - self.k = self.declare(LLVMArrayType(uint8_t, 32)) - self.n = self.declare(LLVMArrayType(uint8_t, 16)) - - self.k_p = self.declare_pointer(LLVMArrayType(uint8_t, 32)) - self.n_p = self.declare_pointer(LLVMArrayType(uint8_t, 16)) - self.ks_p = self.declare_pointer(LLVMArrayType(uint8_t, 64)) - self.points_to(self.k_p, self.k) - self.points_to(self.n_p, self.n) +class ExpandContract(Contract): + def specification(self): + k = self.fresh_var(LLVMArrayType(i8, 32)) + n = self.fresh_var(LLVMArrayType(i8, 16)) + k_p = self.alloc(LLVMArrayType(i8, 32)) + n_p = self.alloc(LLVMArrayType(i8, 16)) + ks_p = self.alloc(LLVMArrayType(i8, 64)) + self.points_to(k_p, k) + self.points_to(n_p, n) - def call(self): - self.arguments(self.k_p, self.n_p, self.ks_p) + self.execute_func(k_p, n_p, ks_p) - def post(self): self.returns(void) - self.points_to(self.ks_p, self.cryptol("Salsa20_expansion`{a=2}")((self.k, self.n))) + self.points_to(ks_p, cryptol("Salsa20_expansion`{a=2}")((k, n))) expand_result = llvm_verify(mod, 's20_expand32', ExpandContract(), lemmas=[hash_result]) @@ -162,24 +130,15 @@ class Salsa20CryptContract(Contract): def __init__(self, size): super().__init__() self.size = size - self.zero = self.cryptol("0 : [32]") - - def val_and_pointer(self, t): - v = self.declare(t) - p = self.declare_pointer(t) - self.points_to(p, v) - return (v, p) - def pre(self): - (self.k, self.k_p) = self.val_and_pointer(LLVMArrayType(uint8_t, 32)) - (self.v, self.v_p) = self.val_and_pointer(LLVMArrayType(uint8_t, 8)) - (self.m, self.m_p) = self.val_and_pointer(LLVMArrayType(uint8_t, self.size)) + def specification(self): + (k, k_p) = ptr_to_fresh(self, LLVMArrayType(i8, 32)) + (v, v_p) = ptr_to_fresh(self, LLVMArrayType(i8, 8)) + (m, m_p) = ptr_to_fresh(self, LLVMArrayType(i8, self.size)) - def call(self): - self.arguments(self.k_p, self.v_p, self.zero, self.m_p, self.cryptol(str(self.size) + " : [32]")) + self.execute_func(k_p, v_p, cryptol('0 : [32]'), m_p, cryptol(f'{self.size!r} : [32]')) - def post(self): - self.returns(self.zero) - self.points_to(self.m_p, self.cryptol("Salsa20_encrypt")((self.k, self.v, self.m))) + self.returns(cryptol('0 : [32]')) + self.points_to(m_p, cryptol("Salsa20_encrypt")((k, v, m))) crypt_result = llvm_verify(mod, 's20_crypt32', Salsa20CryptContract(63), lemmas=[expand_result]) diff --git a/saw-remote-api/test-scripts/saw-test.py b/saw-remote-api/test-scripts/saw-test.py index 53c6e1c93a..bfb96cdd24 100644 --- a/saw-remote-api/test-scripts/saw-test.py +++ b/saw-remote-api/test-scripts/saw-test.py @@ -31,7 +31,7 @@ "post conds": [], "post allocated": [], "post points tos": [], - "return val": {"setup value": "null value"} + "return val": {"setup value": "null"} } prover = ProofScript([abc]).to_json() diff --git a/saw-remote-api/test-scripts/swap.py b/saw-remote-api/test-scripts/swap.py index 272da1ec0c..c3554ba168 100644 --- a/saw-remote-api/test-scripts/swap.py +++ b/saw-remote-api/test-scripts/swap.py @@ -12,31 +12,31 @@ c.llvm_load_module('m', swap_bc).result() -uint32_t = {"type": "primitive type", "primitive": "integer", "size": 32} +i32 = {"type": "primitive type", "primitive": "integer", "size": 32} # ServerNames xp_name = {"name": "xp"} yp_name = {"name": "yp"} # SetupVals -xp = {"setup value": "saved", "name": "xp"} -yp = {"setup value": "saved", "name": "yp"} +xp = {"setup value": "named", "name": "xp"} +yp = {"setup value": "named", "name": "yp"} x = {"setup value": "Cryptol", "expression": "x" } y = {"setup value": "Cryptol", "expression": "x" } contract = { "pre vars": [ - {"server name": "x", "name": "x", "type": uint32_t}, - {"server name": "y", "name": "y", "type": uint32_t} + {"server name": "x", "name": "x", "type": i32}, + {"server name": "y", "name": "y", "type": i32} ], "pre conds": [], "pre allocated": [ {"server name": "xp", - "type": uint32_t, + "type": i32, "mutable": True, "alignment": None}, {"server name": "yp", - "type": uint32_t, + "type": i32, "mutable": True, "alignment": None} ], diff --git a/saw-remote-api/test-scripts/swap_easy.py b/saw-remote-api/test-scripts/swap_easy.py index 8f95ad6d24..83aa513137 100644 --- a/saw-remote-api/test-scripts/swap_easy.py +++ b/saw-remote-api/test-scripts/swap_easy.py @@ -1,5 +1,6 @@ from saw import * -from saw.llvm import uint32_t, Contract, void +from saw.llvm import Contract, void +from saw.llvm_types import i32 import os import os.path @@ -11,22 +12,18 @@ class Swap(Contract): def __init__(self) -> None: super().__init__() - self.t = uint32_t - - def pre(self) -> None: - self.x = self.declare(self.t) - self.y = self.declare(self.t) - self.x_pointer = self.declare_pointer(self.t) - self.y_pointer = self.declare_pointer(self.t) - self.points_to(self.x_pointer, self.x) - self.points_to(self.y_pointer, self.y) - - def call(self) -> None: - self.arguments(self.x_pointer, self.y_pointer) - - def post(self) -> None: - self.points_to(self.x_pointer, self.y) - self.points_to(self.y_pointer, self.x) + self.ty = i32 + + def specification(self) -> None: + x = self.fresh_var(self.ty, "x") + y = self.fresh_var(self.ty, "y") + x_ptr = self.alloc(self.ty, points_to=x) + y_ptr = self.alloc(self.ty, points_to=y) + + self.execute_func(x_ptr, y_ptr) + + self.points_to(x_ptr, y) + self.points_to(y_ptr, x) self.returns(void) env_connect_global() diff --git a/saw-remote-api/test-scripts/swap_fancy.py b/saw-remote-api/test-scripts/swap_fancy.py index 1be18c8fb5..fcaf24e56c 100644 --- a/saw-remote-api/test-scripts/swap_fancy.py +++ b/saw-remote-api/test-scripts/swap_fancy.py @@ -1,7 +1,8 @@ import os import os.path import saw.connection as saw -from saw.llvm import uint32_t, Contract, void +from saw.llvm import Contract, void +from saw.llvm_types import i32 from saw.proofscript import * from env_server import * @@ -16,22 +17,18 @@ class Swap(Contract): def __init__(self) -> None: super().__init__() - self.t = uint32_t - - def pre(self) -> None: - self.x = self.declare(self.t) - self.y = self.declare(self.t) - self.x_pointer = self.declare_pointer(self.t) - self.y_pointer = self.declare_pointer(self.t) - self.points_to(self.x_pointer, self.x) - self.points_to(self.y_pointer, self.y) - - def call(self) -> None: - self.arguments(self.x_pointer, self.y_pointer) - - def post(self) -> None: - self.points_to(self.x_pointer, self.y) - self.points_to(self.y_pointer, self.x) + self.ty = i32 + + def specification(self) -> None: + x = self.fresh_var(self.ty) + y = self.fresh_var(self.ty) + x_ptr = self.alloc(self.ty, points_to=x) + y_ptr = self.alloc(self.ty, points_to=y) + + self.execute_func(x_ptr, y_ptr) + + self.points_to(x_ptr, y) + self.points_to(y_ptr, x) self.returns(void) contract = Swap()