* Update hevm and enable arithmetic abstraction internally
* Test arithmetic abstraction on multiplication monotonicity
* Optimize hevm while preserving symbolic Keccak preimages
Integrate the optimization settings and conditional preimage recording from PR #1621. Keep recording throughout symbolic campaigns and verify that both solvers recover earlier transaction inputs after replaying a symbolic counterexample.
* feat: add a call-sequence syntax for MCP clients
Something driving a campaign from outside it needs a way to name a
sequence of calls, and the natural one is how the calls would be written
in Solidity, with a hole wherever the fuzzer should choose:
approve(0x10, ?); transferFrom(?, ?, 100)
Echidna.MCP.Parse reads that into the list of SolCallPrototypes the
preceding commits taught the fuzzer to generate from. Parsing stops at an
argument's shape rather than its type -- an integer becomes a uint256, an
0x-prefixed literal an address -- because an argument left open carries no
type to compare against anyway, so a prototype is resolved against the
ABI by name and arity either way.
It is a module of its own rather than part of the server that will use
it. This is the one piece of the interface with a set of edge cases worth
enumerating, and Tests.MCPParse enumerates them without needing a
campaign to run against.
Three things differ from the version this is adapted from. `foo(1` no
longer parses as a call with no arguments: the closing parenthesis is
checked rather than assumed, which is what that silently relied on. An
empty sequence is rejected instead of accepted as a sequence of no calls.
And splitting on `;` is Data.List.Split's job rather than a hand-rolled
splitter's -- the bracket-aware split of an argument list still needs its
own, since a comma inside `[1,2]` does not separate arguments.
Nothing parses a sequence yet; the MCP server that does arrives next.
Co-authored-by: gustavo-grieco <[email protected]>
* feat: replace the events server with an MCP server
--server PORT has run a Server-Sent Events server: a one-way stream of
campaign events, enough to watch a campaign with but not to ask it
anything. Replace it with a Model Context Protocol server on the same
flag and the same port, so what is on the other end can both read the
campaign and steer it.
Nine tools. Four report: status (corpus size, iterations, coverage,
tests, optimization values, how long since the last coverage, the
functions that found it, and whatever is being sampled), target,
show_coverage and dump_lcov. Five act: inject_fuzz_transactions and
clear_fuzz_priorities aim the fuzzer at an ordering, sample starts and
stops recording what a function does, execute_sequence replays a concrete
sequence without disturbing the campaign, and reload_corpus picks up
whatever was written to the corpus directory since it started.
The five that act do so over the inter-worker bus, which is why this
comes last: the commands they send, the sampling they switch on and the
replay they ask for all landed in the preceding commits with nothing to
send them. AgentId gains ServerId to say where they come from.
Retiring SSE is the point of the commit rather than a side effect of it.
Echidna.Server had no other caller, so it goes, and wai-extra with it.
The "Waiting until all SSE are received..." drain at the end of a
non-interactive run goes too, and with no reader left the MVar the SIGINT
handler filled goes as well. --server and the `server` config key keep
their names and their meaning -- a port to serve the campaign on -- so
there is no point at which the flag does nothing.
On the dependency: mcp-server comes from Hackage at 0.2.0.1, not from the
personal fork this was prototyped against. Upstream has since released
the two fixes that fork existed for (202 with no body for a notification,
405 for a server-stream GET), so there is no reason to carry a fork of a
library in the closure of a security tool. It needs http-types >= 0.12.6,
which nixpkgs and lts-23.24 both predate: only that version re-exports
`hOrigin` from the umbrella Network.HTTP.Types module that mcp-server
imports unqualified, and http-types has to move for the whole package set
rather than for mcp-server alone, since wai and warp exchange its Status
type with it. Everything in the closure builds against 0.12.6.
Some notes on the shape of it:
The server runs mcpApplication under Warp directly instead of
runMcpServerHttpWithConfig, which announces itself with a bare putStrLn.
Going through a ServerLog event instead keeps the line timestamped and
prefixed like every other one, and leaves Warp's settings to us -- which
matters for binding to loopback.
Origin validation is on with an empty allow-list. The campaign is
reachable from a browser on the same machine, and a page must not be able
to drive a fuzzer through DNS rebinding; a client that sends no Origin at
all, which is every CLI agent, is unaffected.
A tool that cannot do what it was asked answers with an MCP error result
rather than with a report whose text begins "Error:", so a model does not
have to read prose to notice. That is what the Either in ToolRun is.
reload_corpus reads the same two directories the campaign read at
startup, through loadInitialCorpus, rather than the corpus directory
itself -- what is directly in there is those directories, and reading one
as a file is an exception. It decides what is new and adds it inside a
single atomicModifyIORef', because workers are adding to the corpus while
it runs and a read followed by a write would drop whatever arrived in
between. Sequences from disk take the weight of the best entry already
there, never zero, which selectFromCorpus would never draw.
The upstream version's Env.sourceCache is not here: DappInfo already
carries the source cache, so env.dapp.sources is the same thing without a
second copy in Env. Its DumpLcov bus command is not here either -- the
tool calls saveLcovSnapshot directly, and a command with no sender is
what the earlier commits have been leaving out. Its markLines change is
not here: dropping the line number and column separator to save an
agent's tokens would have regressed every text and HTML coverage report
Echidna writes, and an agent that cannot cite a line number is worse off
than one reading a few more tokens.
The recently-covered functions are kept with takeStrict, not take. They
are appended to on every coverage event and read only when a client asks,
so a lazy tail would retain every sequence the campaign ever found
coverage with -- the same trap the sampling state was written around.
One limitation worth knowing: execute_sequence sends every call to the
contract under test, so a sequence naming a function of some other
deployed contract goes to the wrong address. The sequence syntax has no
way to spell an address, so there is nothing to fix it with yet.
Co-authored-by: gustavo-grieco <[email protected]>
* fix: coerce concrete MCP arguments to ABI parameter types
Resolve concrete replay calls against the ABI before constructing SolCall values, and coerce fixed arguments in fuzz prototypes. Preserve signed and full-width literals, validate bounds and array lengths, and reject ambiguous replay overloads.
Add parser, coercion, mixed-prototype and Solidity replay regressions. The focused 63-test suite and live MCP probe pass; restoring the original call construction fails all four call-site regression tests.
* test: cover bytes32 literals in mixed MCP calls
Exercise asymmetric 32-byte words through generic mixed-parameter replay and injected prototypes. Check leading-zero padding, the zero word, and oversized literal rejection for G3, whose implementation is covered by the B1 coercion fix.
Validation: targeted HLint and git diff --check pass. Execution testing is deferred to GitHub CI.
* fix: start MCP only after workers are ready
---------
Co-authored-by: gustavo-grieco <[email protected]>
* Bump tls to 2.2.2 in flake and stack
tls < 2.2.2 is affected by https://github.com/haskell-tls/hs-tls/pull/515.
tls 2.2.2 needs the crypton-x509 1.8 line, which still builds against
crypton 1.0.x (the 1.9 line would force crypton >= 1.1 and a much wider
cascade). No crypton-connection release targets tls 2.2 (0.4.5 caps < 2.2,
0.4.6 needs >= 2.3), so its tls < 2.2 bound is relaxed, along with
warp-tls and tls-session-manager (pulled in by Hoogle in the dev shell);
all compile fine against 2.2.2.
In flake.nix the codegen cabal2nix is pinned to the un-overridden base
set, otherwise regenerating tls via callHackageDirect loops (cabal2nix
transitively depends on tls). stack.yaml additionally pins the
crypton-asn1-*/crypton-pem/time-hourglass/hpke/ech-config packages that
lts-23.24 lacks; nixpkgs-unstable already carries compatible versions.
* Add crypton-socks-0.6.2 extra-dep for stack
crypton-connection 0.4.5 needs crypton-socks >= 0.6, which lts-23.24 does
not provide. Matches the version the flake already resolves.
* Fix suitableForSymExec precedence inversion
`not $ null m.inputs && ...` parsed as `not (null m.inputs && ...)`,
negating the whole conjunction: the dynamic-argument guard never fired
(so bytes/string/dynamic-array methods were handed to the symbolic
encoder, which throws).
Bind `not` to the emptiness check alone so the filter means what it
says: explore methods that have arguments, none dynamic, not opted out.
* updated to new hevm
* dynamic array handling
* Update hevm in flake.nix
---------
Co-authored-by: gustavo-grieco <[email protected]>
* improved support for foundry tests
* Extend Foundry support testing (#1512)
* Fix lint failures
* ci: bump python version to 3.10, clone submodules
* some fixes when using foundry mode
* Update hevm to `542986dea3bec4f5898731ff48877a7a21811bf4`
* Fix bugs in Foundry test generation (#1516)
* Fix fallback function bug in Foundry test generation
* Fix null byte in argument bug in Foundry test generation
* Remove unnecessary config file
* Remove unused/redundant imports
* Disable Slither in Foundry test gen tests
* Conditionally run forge-std tests based on the solc version
* Reduce unnecessary test grouping and improve failed assertion messages
---------
Co-authored-by: Emilio López <[email protected]>
* Update hevm to `41e6d1304411749ea8c816d131991663b5dca67a`
* Fix linter and build errors (#1521)
* improve foundry stateful invariant testing
* fix
* Fix foundry test generation linter hints and tests (#1522)
* Foundry updates (#1525)
* Rename dapptest to foundry and support foundry assertX in assertion mode
* Rename basic foundry test contracts dir to `foundry-basic`
* Add testing modes to `README`
* fixes
* fixes
* Add support for Foundry assume (#1528)
* flake: sync hevm version with stack.yaml
* Clarify `optimization` test mode in `README` (#1529)
* IS_TEST fix
---------
Co-authored-by: Radu Bahmata <[email protected]>
Co-authored-by: Emilio López <[email protected]>
Co-authored-by: Emilio López <[email protected]>
* Upgrade `hevm` to `95b5e074c9f27f970011ed53f38f1643d70c3c8a`
* Refactor cache use after hevm upgrade
* fixes
* Added rpc cache serialization code and fixes
* fixes
* fixes
* fixes
* refactor verification code to make sure tests are correctly labeled when the verifiction finishes
* revert b899481b65
* disable RPC logs
* update to the latest hevm
* updated flake
* updated flake
* avoid crashing when trying to do symbolic execution in fallback
* silence RPC warning when there is no RPC configured
* hlint fixes
* switch to stack based loop detection
* Clean up comment, whitespace
---------
Co-authored-by: Emilio López <[email protected]>
* removed old solc versions, use 0.8.x only instead
* fixed harvey test
* started to fix symexec using latest hevm
* added RPC support for symbolic execution + some clean up
* better constraints for block timestamp and number
* improved and simplified symexec code
* removed useless code
* some test fixes
* increase the number of random symbolic transaction if the corpus is empty
* added comments on why we only take one method from the shuffle list when doing symbolic exploration
* allow user to select smt solver
* use slither to filter functions with assert, if any
* started adding full verification mode for stateless campaigns
* refactored tons of code
* improved code for exploration/verification
* finished implementation and get back to hevm master
* fixed issue in addBlockConstraints and upgraded hevm
* disable debug mode when using interactive mode
* corrected array size in symbolic output
* fix decoding of negative numbers
* simplified code for decoding of negative numbers
* removed initialize field from default
* use verification mode for sym-assert test
* added some basic verification tests
* make the harvey test more reliable
* simplified exploration code and added shrinking
* added new test for exploration mode (but disabled so far)
* worker related refactoring code to allow other parts of the codebase to send events
* make sure symExecTarget is used to select methods
* keccak preimage support enabled
* reduced code duplication
* added documentation
* use new types in Types/Config.hs
* removed killed-related files
* Upgrade hevm to latest `echidna-patches` commit
* Upgrade build to GHC 9.6
* Refactor terminal and signal support in preparation for Windows UI
* Enable UI on all platforms
* Use pkgsStatic for Linux
pkgsMusl fails to build for some reason.
* Remove conditional UI compilation
All platforms now support the Echidna UI
* Enable UI on ConHost as well
See the introduction on https://hackage.haskell.org/package/ansi-terminal-1.1.1/docs/System-Console-ANSI.html
* Enable `eager-blackholing`
Observed a ~2% speedup on longer runs when compiling both hevm and
echidna with this flag. Besides, the Haskell documentation encourages
enabling it for parallel code:
https://downloads.haskell.org/~ghc/9.6.5/docs/users_guide/using-concurrent.html#compile-time-options-for-smp-parallelism
* Resolve hlint warnings
* Update Linux Stack CI to 9.6
* Fix compilation failure after merge
* Upgrade hevm to `echidna-patches-20240725`
* Fix lint warnings, unused imports
* flake: align nixpkgs with hevm
* flake: fix libiconv for x86_64 darwin
> app/utf8-troubleshoot/cbits/locale.c:10:10: error:
> fatal error: 'libcharset.h' file not found
> |
> 10 | #include <libcharset.h>
> | ^
> #include <libcharset.h>
> ^~~~~~~~~~~~~~
Also link iconv dynamically on Darwin as well
* switch to tstore branch on hevm fork. all we should need now is a call to clearTStorages
* call clearTStorages after each transaction
* test case
* bump hevm
* bump hevm again
---------
Co-authored-by: Sam Alws <[email protected]>
* Update to GHC 9.4
* ci: Update to GHC 9.4
* ci: fix GHC 9.4 support on Windows
GHC 9.4 has changed toolchains to Clang, which causes issues when building
with our current setup. We perform the following changes to support
GHC 9.4 and later:
* Use MSYS2 CLANG64 MSYS. See https://gitlab.haskell.org/ghc/ghc/-/issues/22561
* Use MSYS2 minimal $PATH. There's many things in the default GitHub
environment that cause conflicts. To achieve this, we have to also
manually re-add the Stack, Cabal and GHC paths.
* Bump the Stack resolver. GHC 9.4.7 has some compilation fixes that
are good to have around.
* Replace the GHC linker with our MSYS2 linker. The GHC linker is old
(~LLVM 14?) and does not fully understand the static libraries
produced by the newer Clang 17 in MSYS2.
* Refactor the way we invoke Stack and take advantage of the Stack
config to indicate extra library and include paths.
* Drop the 'strip' workaround for the test suite, as it is not needed
any longer.
* Fix the linking of the standard C++ library. GHC 9.4 introduces a
nice way to do it in a platform-independent way, but unfortunately
it does not work properly in Nix and it attempts to link clang++
instead of libc++.so, so we have to use some trickery.
addDLL: stdc++ or dependencies not loaded. (Win32 error 126)
See also:
* https://gitlab.haskell.org/ghc/ghc/-/issues/22738
* https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.4?version_id=b60e52482a666d25638d59cd7e86851ddf971dc1#link-against-system-cxx-std-lib-instead-of-stdc
* hevm: pin to newer version supporting GHC 9.4
* ci: linux: update to GHC 9.4.7
* ci: do not cache Stack config
---------
Co-authored-by: Emilio López <[email protected]>
Gustavo Grieco