Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proxied token formal verification #71 #75

Merged
merged 14 commits into from Nov 23, 2018

Conversation

Projects
None yet
3 participants
@daejunpark
Copy link
Collaborator

commented Nov 20, 2018

reissue #71

@denis-bogdanas
Copy link
Contributor

left a comment

As a conclusion, the specification contains rewrites of balance that can hide abusive behavior and is thus incomplete. Also the way failure is handled is a deviation from recommended behavior (because the standard says SHOULD throw etc..) and should be clearly described in readme and also mentioned to the users of this token.

// An Ethereum address X has an address space of [0, 2^160). Hence if we do (2^256 - 1) - (2^160 - 1) &Int X, the result will always be 0.

rule 115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int => 0
requires #rangeAddress(X)

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

Please add a comment explaining the meaning of this number - e.g. its hex value.
Also, for all other lemmas please explain in comments where are they needed to the extent you know.

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

First point - done. Second point - honestly I don't remember, but I'll keep a record of this next time.

[changeMasterCopy-failure-2]
; function called by address different from creator
+requires:
andBool #rangeAddress(NEW_MASTER_COPY_ID)

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

duplicate range predicate.
Also this spec is ambiguous to read. Please explicitly add msg_sender value here, even if it is inherited.

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

done

+requires:
andBool 0 <Int NEW_MASTER_COPY_ID

[changeMasterCopy-failure]

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

empty intermediate specs like this have no effect. Please delete.

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

done

callValue: CALL_VALUE
+requires:
andBool #rangeUInt(256, CALL_VALUE)
andBool 0 <Int CALL_VALUE

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

This sort of failure specs also look ambiguous. Please add status code specification for all.

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

done

output: _ => #asByteStackInWidth(0, 32)
[transfer-failure-1]
+storage:
#hashedLocation({COMPILER}, {_BALANCES}, RANDOM_ID) |-> (BAL_FROM => _)

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

is BAL_FROM changing in case of failure??

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

this was an actual bug. good catch!

andBool ( VALUE >Int BAL_FROM
orBool BAL_TO +Int VALUE >=Int (2 ^Int 256) )

[transfer-failure-2]

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

how is this a failure?

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

both transfer-failure-1 and transfer-failure-2 are failures because the math overflows, so the arithmetic checks would return false (see first few lines of transfer fn in deployed.sol)

#hashedLocation({COMPILER}, {_BALANCES}, TO_ID) |-> BAL_TO
+requires:
andBool ( VALUE >Int BAL_FROM
orBool BAL_TO +Int VALUE >=Int (2 ^Int 256) )

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

Use pow256 here.

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

Also, looks like status is EVMC_SUCCESS, inherited from [transfer]. In this case the token does not comply with ERC20. Please correct me if I'm wrong. Same for other failure rules.

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

pow256 - done
It does comply with ERC20- the definition of compliance is that it implements all MUST clauses. Throwing is a SHOULD clause.

andBool BAL_FROM +Int VALUE <Int (2 ^Int 256)

[transfer-failure]
output: _ => #asByteStackInWidth(0, 32)

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

add a comment: ; return false

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

done

andBool 0 <Int CALL_VALUE

[transfer]
statusCode: _ => EVMC_SUCCESS

This comment has been minimized.

Copy link
@denis-bogdanas

denis-bogdanas Nov 21, 2018

Contributor

Explain in a comment why return status is success even for most failure rules - because return value false is used instead to denote failure.

This is a difference from behavior recommended in the standard and should be noted in the readme. Please describe precisely the failure cases where functions return false instead of THROW.

This comment has been minimized.

Copy link
@dteiml

dteiml Nov 22, 2018

Collaborator

done

@denis-bogdanas

This comment has been minimized.

Copy link
Contributor

commented Nov 22, 2018

Also please rebase both PRs on master. Gnosis branch is work in progress.

@dteiml

This comment has been minimized.

Copy link
Collaborator

commented Nov 23, 2018

Also please rebase both PRs on master. Gnosis branch is work in progress.

It is already rebased on master. My first commit Finished proxied token e1975 has as parent testEcrecover full specification (#69) 995d4, latest master commit

@denis-bogdanas denis-bogdanas merged commit 39c1312 into master Nov 23, 2018

1 check passed

rvk jenkins
Details

@denis-bogdanas denis-bogdanas deleted the proxied-token branch Nov 23, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.