• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
          • Command-error
          • Sign
          • Init-from-mnemonic
          • Command-error-message
          • Stat
          • Next-key
          • Init-from-entropy
          • Process-command
          • Transaction-message
          • Maybe-command-error
          • Maybe-stat
          • Check-stat-file-present
          • Valid-key-path-p
          • String-to-byte-list
          • Load-stat
          • Mnemonic-message
          • Process-sign
          • Process-init-from-entropy
          • All-valid-key-paths-p
          • String-to-word
          • String-to-nat
          • Process-next-key
          • Wallet
          • Process-init-from-mnemonic
          • Check-stat-file-absent
          • Stat-wfp
          • Save-stat
          • Stat-addresses-bounded-p
          • Stat-all-valid-key-paths-p
          • Stat-priv-keys-p
          • Stat-root-depth-zero-p
          • Stat-path-prefix-in-tree-p
          • Crypto-hdwallet-executable
          • *stat-filepath*
          • *key-path-prefix*
          • *coin-type-index*
          • *purpose-index*
          • *external-chain-index*
          • *command-name-init-from-mnemonic*
          • *command-name-init-from-entropy*
          • *account-index*
          • *command-name-sign*
          • *command-name-next-key*
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Kestrel-books

Crypto-hdwallet

A hierarchical deterministic wallet for cryptocurrencies.

Overview

This wallet is a simple proof of concept: it is not meant as a product to use with keys that control access to significant assets. Nonetheless, due to its formal basis in the ACL2 theorem prover, it could serve as a starting point for a high-assurance wallet product.

This wallet is meant for use on an air-gapped machine. It provides two basic functions: key generation and transaction signing. Thus, keys can be generated and used for signing transacions: the data of the transaction to sign and the signed transaction must be passed between the air-gapped machine where this wallet runs and an Internet-connected machine that submits the signed transactions. The private keys never leave the air-gapped machine. Currently, the wallet does not encrypt these keys, which are stored in plaintext in the file system: therefore, the air-gapped machine should use disk encryption to protect the keys at rest. Currently keys and transactions only for the Ethereum mainnet are supported.

The wallet is hierarchical deterministic, according to BIP 32. It uses a mnemonic word sequence according to BIP 39. Its internal structure is compliant with BIP 43 and BIP 44.

The wallet can be run by a command line interface shell script that runs a Docker image containing the wallet code. For details on obtaining, installing, and running the wallet see the README in GitHub. The following is a technical discussion of the current wallet design.

State

The state of the wallet consists of zero or more private keys derived from a seed as in BIP 32. The seed is derived from an entropy value, or a corresponding mnemonic, as in BIP 39. Internally, each key has a path of the form

m / 44' / 60' / 0' / 0 / address_index

where:

  • 44' is the BIP 43 purpose index for BIP 44.
  • 60' is the coin type index for the Ethereum mainnet, as prescribed by SLIP (Satoshi Labs Improvement Proposal) 44. This wallet currently supports transactions only for the Ethereum mainnet, as mentioned above.
  • 0' is the default account index, according to BIP 44. The wallet currently supports only this default account.
  • 0 is the external chain index, according to BIP 44. For Ethereum, unlike Bitcoin, there should be no need for an internal chain index, since transactions involve no change back to the payer.
  • address_index is an address index 0, 1, 2, ... Each of these has an associated Ethereum account and address.

Thus, the BIP 32 key tree in the wallet consists of a ``line'' from the root key to the external chain key, with zero or more children under that.

The state of the wallet also includes a counter for the number of address indices used so far. This is normally one above the largest address index in the key tree, except for the rare cases in which an address key derivation fails and that index must be skipped. This counter is normally redundant, but not always.

Initialization

The wallet provides two commands to initialize the wallet. The first command initializes the wallet from an entropy value and a passphrase, as described in BIP 39. Besides creating the initial key tree (initially without address keys), this command also outputs the mnemonic corresponding to the entropy value. This may be used by the second initialization command to reconstruct (i.e. re-initialize) the wallet, from the mnemonic and the passphrase, also as described in BIP 39.

It is expected that the user will initially use the first initialization command, and use the second initialization command only if and when the wallet must be re-created. The wallet currently does not provide facilities to generate a securely random entropy: the user must use external means for that, and pass the entropy to the wallet.

In rare cases, the initialization of the wallet from entropy and passphrase may fail, due to the failure to derive some key on the ``line'' from the root (master) key to the external chain key. In this case, the user must try again with a slightly different entropy or passphrase. Obviously, if a particular entropy and passphrase succeed in creating the wallet with the first initialization command, then the mnemonic corresponding to that entropy and the same passphrase will also succeed in creating the same wallet using the second initialization command.

Key Generation

Once the wallet is initialized as explained above, the user must create one or more address keys in order to sign transactions (see below). The wallet provides a command to generate the next address key, namely the key whose index is the aforementioned counter that is part of the wallet state along with the key tree. Since the counter is initially 0, the first address key to be generated is the one with index 0, then index 1, then index 2, etc.

Normally, the generation of an address key succeeds. In this case, besides modifying the internal state of the wallet, the command also outputs the index of the key (so that the user does not need to keep track of the counter, or next index), as well as the Ethereum address corresponding to the key. The address is derived from the public key (as explained in the Ethereum Yellow Paper), which is derived from the private key (as known in elliptic curve cryptography).

In rare cases, the generation of an address key may fail. In this case, the address index is simply skipped, and the counter (i.e. next key) is advanced so that the command can be tried again to generate the next key.

Transaction Signing

Once at least one address key has been generated (normally the one with index 0), the command to sign transactions can be used. The index of the address key to use for the signature is passed to the signing command by the user.

The signing command also takes as inputs the following components of the transaction (see the Ethereum Yellow Paper for details):

  • The nonce associated to the Ethereum address. This is stored in the state of the Ethereum network, but since this wallet is air-gapped, the user must keep track of the nonce, and supply it to the signing command.
  • The gas price for processing the transaction. This is under the user's discretion.
  • The gas limit for processing the transaction. This should be accurately estimated by the user, plausibly with the aid of some tools external to the wallet.
  • The recipient address. The address may be that of a contract or of an externally owned account; the wallet supports both.
  • The value to transmit to the recipient, in Wei.
  • The data (a sequence of bytes) to pass to the recipient. This makes sense when the recipient is a contract, as opposed to an externally owned account.

The command outputs the bytes of the signed transaction, RLP-encoded. This is the form in which the transaction must be submitted to the Ethereum network. Since this wallet is air-gapped, the user must copy the output of this command and use an Internet-connected machine to actually submit the transaction.

In rare cases, the signing of the transaction may fail. Since the elliptic curve signature scheme used by this wallet is deterministic, re-trying the same command will fail again. Instead, the user could try to change slightly some non-critical component of the transaction, such as the gas limit.

Persistence

This wallet runs in ``batch'' mode: each command starts up the wallet, which terminates at the end of the command. The state of the wallet must be therefore stored persistently, in a file in the file system. The ACL2 constant *stat-filepath* holds the path to this file: it is currently set to a relative path in this directory, but it can be easily changed of course.

Currently the file stores the wallet state in plaintext, i.e. not encrypted. Future versions of the wallet will likely use AES encryption. However, recall that this wallet is meant for an air-gapped machine: at rest, the wallet state can be protected by disk encryption. Thus, even if the machine is stolen, it should not be possible to recover the wallet state, assuming that the disk encryption is protected by a strong password.

Error Handling

The wallet carefully validates all the user inputs and provides informative error messages when the inputs are invalid. The wallet also provides informative error messages when some internal cryptographic operation fails due to a rare but possible event (as mentioned above). There is just one exception to this approach to error handling: in order to load/save the wallet state from/to the file, the wallet implementation uses ACL2's serialize-read and serialize-write, which may throw hard errors in some cases. Thus, it is currently possible, but hopefully rare, to get an ACL2 hard error from the wallet.

Subtopics

Command-error
Possible command errors.
Sign
Transaction signature in the wallet.
Init-from-mnemonic
Initialization of the wallet from a mnemonic (and passphrase).
Command-error-message
Turn a command error into a user-oriented message.
Stat
State of the wallet.
Next-key
Address key generation in the wallet.
Init-from-entropy
Initialization of the wallet from an entropy value (and a passphrase).
Process-command
Process a command.
Transaction-message
Build a message that describes a (signed) transaction.
Maybe-command-error
Union of command errors and nil.
Maybe-stat
Union of wallet states and nil.
Check-stat-file-present
Ensure that the wallet state file exists.
Valid-key-path-p
Check if a key path is valid for the wallet.
String-to-byte-list
Parse a string into a list of bytes.
Load-stat
Load the state of the wallet from a file.
Mnemonic-message
Build a message that describes a generated mnemonic.
Process-sign
Process a transaction signing command.
Process-init-from-entropy
Process a command to initialize the wallet from an entropy value.
All-valid-key-paths-p
Lift valid-key-path-p to sets of paths.
String-to-word
Parse a string into a word.
String-to-nat
Parse a string into a natural number.
Process-next-key
Process a key generation command.
Wallet
Entry point to the ACL2 code of the wallet.
Process-init-from-mnemonic
Process a command to initialize the wallet from a mnenonic.
Check-stat-file-absent
Ensure that the wallet state file does not already exist.
Stat-wfp
All the constraints on the wallet state.
Save-stat
Save the state of the wallet to a file.
Stat-addresses-bounded-p
Constraint on the number of address keys in the wallet state.
Stat-all-valid-key-paths-p
Check if all the key paths in the wallet are valid.
Stat-priv-keys-p
Constraint on the kind of keys in the wallet state.
Stat-root-depth-zero-p
Constraint on the root depth in the wallet state.
Stat-path-prefix-in-tree-p
Constraint on the key path prefix in the wallet state.
Crypto-hdwallet-executable
Executable version of the hierachical deterministic wallet for cryptocurrencies.
*stat-filepath*
Path of the file that stores the state of the wallet.
*key-path-prefix*
The prefix of the path to the address keys of the wallet.
*coin-type-index*
The coin type index of the paths to the address keys of the wallet.
*purpose-index*
The purpose index of the paths to the address keys of the wallet.
*external-chain-index*
The external chain index of the paths to the address keys of the wallet.
*command-name-init-from-mnemonic*
Name of the command to initialize the wallet from a mnemonic.
*command-name-init-from-entropy*
Name of the command to initialize the wallet from an entropy value.
*account-index*
The account index of the paths to the address keys of the wallet.
*command-name-sign*
Name of the command to sign a transaction.
*command-name-next-key*
Name of the command to generate the next key.