Skip to content

Commit 4081e49

Browse files
greenhatgreenhat
authored
Merge pull request #23 from ergoplatform/i13-vuln-tests
Vulneraibility analysis of DEX limit order contracts
2 parents 02f7ca5 + 97c1d5f commit 4081e49

File tree

7 files changed

+637
-35
lines changed

7 files changed

+637
-35
lines changed

‎README.md

Lines changed: 17 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,36 @@
11
# Ergo Contracts
2+
Source code of the Ergo smart contracts with compilation, testing, and formal verification tooling.
23

3-
## Prerequisites:
4+
# List of contracts:
5+
Certified(ErgoScala):
6+
- Assets Atomic Exchange [src](https://github.com/ergoplatform/ergo-contracts/blob/19e23fde8c94a71eb8ca839c829e4efb4e4e63ac/verified-contracts/src/main/scala/org/ergoplatform/contracts/AssetsAtomicExchange.scala#L12-L70) , [verified properties](https://github.com/ergoplatform/ergo-contracts/blob/19e23fde8c94a71eb8ca839c829e4efb4e4e63ac/verified-contracts/src/main/scala/org/ergoplatform/contracts/AssetsAtomicExchange.scala#L72-L141)
7+
- Crowd Funding [src](https://github.com/ergoplatform/ergo-contracts/blob/19e23fde8c94a71eb8ca839c829e4efb4e4e63ac/verified-contracts/src/main/scala/org/ergoplatform/contracts/CrowdFundingContractVerification.scala#L10-L30), [verified properties](https://github.com/ergoplatform/ergo-contracts/blob/19e23fde8c94a71eb8ca839c829e4efb4e4e63ac/verified-contracts/src/main/scala/org/ergoplatform/contracts/CrowdFundingContractVerification.scala#L32-L105)
8+
- ICO Funding [src](https://github.com/ergoplatform/ergo-contracts/blob/19e23fde8c94a71eb8ca839c829e4efb4e4e63ac/verified-contracts/src/main/scala/org/ergoplatform/contracts/ICOContractVerification.scala#L9-L186), [verified properties](https://github.com/ergoplatform/ergo-contracts/blob/19e23fde8c94a71eb8ca839c829e4efb4e4e63ac/verified-contracts/src/main/scala/org/ergoplatform/contracts/ICOContractVerification.scala#L208-L279)
9+
10+
ErgoScript:
11+
- DEX with limit orders and partial matching [src](https://github.com/ergoplatform/ergo-contracts/blob/19e23fde8c94a71eb8ca839c829e4efb4e4e63ac/contracts/src/main/scala/org/ergoplatform/contracts/DexLimitOrder.scala#L45-L315) [docs](https://github.com/ergoplatform/ergo-contracts/blob/19e23fde8c94a71eb8ca839c829e4efb4e4e63ac/contracts/src/main/scala/org/ergoplatform/contracts/DexLimitOrder.scala#L319-L397)
12+
13+
## How to add a new certified contract
14+
Certified contracts are written in ErgoScala (a subset of Scala, compiled with [ErgoScala compiler](https://github.com/ergoplatform/ergo-scala-compiler)) and have their properties verified using formal verification with [Stainless](https://stainless.epfl.ch/).
15+
16+
## Prerequisites for certified contracts:
417
- Install Z3 SMT solver from https://github.com/Z3Prover/z3
518

6-
## How to add a new contract
7-
819
### Create a method for the contract
920
Subclass `SigmaContract` in the `verified-contracts` project and put a contract code in a method. The first parameter has to be `ctx: Context`, and subsequent parameters may be contract parameters. The return value has to be `SigmaProp`. Make the first line of the contract code `import ctx._` to improve readability.
1021

1122
### Write contract code in the method.
1223
See [DEX buy order](http://github.com/ergoplatform/ergo-contracts/blob/71f1ef745b7ffce80272e7050a65ec4f68bfd661/verified-contracts/src/main/scala/org/ergoplatform/contracts/AssetsAtomicExchange.scala#L12-L45) for an example.
1324

14-
### Contract compilation
25+
### Contract compilation (ErgoScala)
1526
Create a subclass (object) of the class with contract code to make an "instance" method to compile the contract's code.
1627
It'll invoke the compiler (macros) and returns a compiled contract with embedded contract parameters. Create a method with parameters from the contract (without the `Context` parameter) and invoke `ErgoContractCompiler.compile`. See [DEX buy order](http://github.com/ergoplatform/ergo-contracts/blob/71f1ef745b7ffce80272e7050a65ec4f68bfd661/verified-contracts/src/main/scala/org/ergoplatform/contracts/AssetsAtomicExchange.scala#L150-L158) for an example.
1728
Mark this method with `@ignore` annotation to hide it from Stainless.
1829

1930
### How to use compiled contract
20-
Call the "instance" method in another module/project and it'll return 'ErgoContract'(compiled contract).
31+
Call the "instance" method in another module/project, and it'll return 'ErgoContract'(compiled contract).
2132
Call `ErgoContract.scalaFunc` to run the contract with given `Context`. See [DEX buy order](http://github.com/ergoplatform/ergo-contracts/blob/71f1ef745b7ffce80272e7050a65ec4f68bfd661/verified-contracts-test/src/test/scala/org/ergoplatform/contracts/tests/AssetsAtomicExchangeCompilationTest.scala#L319-L324) for an example.
2233

2334
### Verifying contract properties
24-
Verification is done using [Stainless](https://epfl-lara.github.io/stainless/verification.html). Create a subclass(object) of the class where you put contracts (as methods). Use a method for each property you want to verify. Put pre-conditions in `require()` call, call the contract and verify post-conditions. See [DEX buy order](http://github.com/ergoplatform/ergo-contracts/blob/71f1ef745b7ffce80272e7050a65ec4f68bfd661/verified-contracts/src/main/scala/org/ergoplatform/contracts/AssetsAtomicExchange.scala#L90-L113) verified properties for an example.
35+
Verification is done using [Stainless](https://epfl-lara.github.io/stainless/verification.html). Create a subclass(object) of the class where you put contracts (as methods). Use a method for each property you want to verify. Put pre-conditions in `require()` call, call the contract, and verify post-conditions. See [DEX buy order](http://github.com/ergoplatform/ergo-contracts/blob/71f1ef745b7ffce80272e7050a65ec4f68bfd661/verified-contracts/src/main/scala/org/ergoplatform/contracts/AssetsAtomicExchange.scala#L90-L113) verified properties for an example.
2536

‎contracts/src/main/scala/org/ergoplatform/contracts/DexLimitOrder.scala

Lines changed: 54 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ private object DexLimitOrderErgoScript {
5757

5858
val buyerScript = s"""buyerPk || {
5959

60+
// counter(sell) orders that are matched against this order
6061
val spendingSellOrders = INPUTS.filter { (b: Box) =>
6162
b.R4[Coll[Byte]].isDefined && b.R5[Long].isDefined && {
6263
val sellOrderTokenId = b.R4[Coll[Byte]].get
@@ -66,18 +67,24 @@ private object DexLimitOrderErgoScript {
6667
}
6768
}
6869

70+
// box with mine(bought) tokens
71+
// check that such box is only one in outputs is later in the code
6972
val returnBoxes = OUTPUTS.filter { (b: Box) =>
7073
val referencesMe = b.R4[Coll[Byte]].isDefined && b.R4[Coll[Byte]].get == SELF.id
7174
val canSpend = b.propositionBytes == buyerPk.propBytes
7275
referencesMe && canSpend
7376
}
7477

78+
// check if this order should get the spread for a given counter order(height)
7579
val spreadIsMine = { (counterOrderBoxHeight: Int) =>
7680
// greater or equal since only a strict greater gives win in sell order contract
81+
// Denys: we have to decide who gets the spread if height is equal, without any reason I chose buy order
7782
counterOrderBoxHeight >= SELF.creationInfo._1
7883
}
7984

80-
val boxesAreSortedBySpread = { (boxes: Coll[Box]) =>
85+
// check that counter(sell) orders are sorted by spread in INPUTS
86+
// so that the bigger(top) spread will be "consumed" first
87+
val sellOrderBoxesAreSortedBySpread = { (boxes: Coll[Box]) =>
8188
boxes.size > 0 && {
8289
val alledgedlyTopSpread = if (spreadIsMine(boxes(0).creationInfo._1)) {
8390
tokenPrice - boxes(0).R5[Long].getOrElse(0L)
@@ -86,23 +93,28 @@ private object DexLimitOrderErgoScript {
8693
val prevSpread = t._1
8794
val isSorted = t._2
8895
val boxTokenPrice = box.R5[Long].getOrElse(0L)
96+
val boxTokenPriceIsCorrect = boxTokenPrice > 0 && boxTokenPrice <= tokenPrice
8997
val spread = if (spreadIsMine(box.creationInfo._1)) {
9098
tokenPrice - boxTokenPrice
9199
} else { 0L }
92-
(spread, isSorted && spread <= prevSpread)
100+
(spread, isSorted && boxTokenPriceIsCorrect && spread <= prevSpread)
93101
})._2
94102
}
95103
}
96104

97105
returnBoxes.size == 1 &&
98106
spendingSellOrders.size > 0 &&
99-
boxesAreSortedBySpread(spendingSellOrders) && {
107+
sellOrderBoxesAreSortedBySpread(spendingSellOrders) && {
100108

101109
val returnBox = returnBoxes(0)
110+
// token amount that are bought
102111
val returnTokenAmount = if (returnBox.tokens.size == 1) returnBox.tokens(0)._2 else 0L
103112
113+
// DEX fee that we allow for matcher to take
104114
val expectedDexFee = dexFeePerToken * returnTokenAmount
105115
116+
// in case of partial matching new buy order box should be created with funds that are not matched in this tx
117+
// check that there is only one such box is made later in the code
106118
val foundResidualOrderBoxes = OUTPUTS.filter { (b: Box) =>
107119
val tokenIdParamIsCorrect = b.R4[Coll[Byte]].isDefined && b.R4[Coll[Byte]].get == tokenId
108120
val tokenPriceParamIsCorrect = b.R5[Long].isDefined && b.R5[Long].get == tokenPrice
@@ -114,15 +126,15 @@ private object DexLimitOrderErgoScript {
114126
contractParamsAreCorrect && referenceMe && guardedByTheSameContract
115127
}
116128

129+
// aggregated spread we get from all counter(sell) orders
117130
val fullSpread = {
118131
spendingSellOrders.fold((returnTokenAmount, 0L), { (t: (Long, Long), sellOrder: Box) =>
119132
val returnTokensLeft = t._1
120133
val accumulatedFullSpread = t._2
121134
val sellOrderTokenPrice = sellOrder.R5[Long].get
122135
val sellOrderTokenAmount = sellOrder.tokens(0)._2
123-
val priceIsCorrect = sellOrderTokenPrice <= tokenPrice
124136
val tokenAmountFromThisOrder = min(returnTokensLeft, sellOrderTokenAmount)
125-
if (spreadIsMine(sellOrder.creationInfo._1) && priceIsCorrect) {
137+
if (spreadIsMine(sellOrder.creationInfo._1)) {
126138
// spread is ours
127139
val spreadPerToken = tokenPrice - sellOrderTokenPrice
128140
val sellOrderSpread = spreadPerToken * tokenAmountFromThisOrder
@@ -135,9 +147,13 @@ private object DexLimitOrderErgoScript {
135147
})._2
136148
}
137149

150+
// ERGs paid for the bought tokens
138151
val returnTokenValue = returnTokenAmount * tokenPrice
152+
// branch for total matching (all ERGs are spent and correct amount of tokens is bought)
139153
val totalMatching = (SELF.value - expectedDexFee) == returnTokenValue &&
140154
returnBox.value >= fullSpread
155+
// branch for partial matching, e.g. besides bought tokens we demand a new buy order with ERGs for
156+
// non-matched part of this order
141157
val partialMatching = {
142158
val correctResidualOrderBoxValue = (SELF.value - returnTokenValue - expectedDexFee)
143159
foundResidualOrderBoxes.size == 1 &&
@@ -178,18 +194,24 @@ private object DexLimitOrderErgoScript {
178194

179195
val selfTokenAmount = SELF.tokens(0)._2
180196

197+
// box with ERGs(mine) for sold tokens
198+
// check that such box is only one in outputs is later in the code
181199
val returnBoxes = OUTPUTS.filter { (b: Box) =>
182200
val referencesMe = b.R4[Coll[Byte]].isDefined && b.R4[Coll[Byte]].get == SELF.id
183201
val canSpend = b.propositionBytes == sellerPk.propBytes
184202
referencesMe && canSpend
185203
}
186204

205+
// check if this order should get the spread for a given counter order(height)
187206
val spreadIsMine = { (counterOrderBoxHeight: Int) =>
188207
// strictly greater since equality gives win in buy order contract
208+
// Denys: we have to decide who gets the spread if height is equal, without any reason I chose buy order
189209
counterOrderBoxHeight > SELF.creationInfo._1
190210
}
191211

192-
val boxesAreSortedBySpread = { (boxes: Coll[Box]) =>
212+
// check that counter(buy) orders are sorted by spread in INPUTS
213+
// so that the bigger(top) spread will be "consumed" first
214+
val buyOrderBoxesAreSortedBySpread = { (boxes: Coll[Box]) =>
193215
boxes.size > 0 && {
194216
val alledgedlyTopSpread = if (spreadIsMine(boxes(0).creationInfo._1)) {
195217
boxes(0).R5[Long].getOrElse(0L) - tokenPrice
@@ -198,12 +220,15 @@ private object DexLimitOrderErgoScript {
198220
val prevSpread = t._1
199221
val isSorted = t._2
200222
val boxTokenPrice = box.R5[Long].getOrElse(0L)
223+
// although buy order's DEX fee is not used here, we check if its positive as a part of sanity check
224+
val boxDexFeePerToken = box.R6[Long].getOrElse(0L)
201225
val spread = if (spreadIsMine(box.creationInfo._1)) { boxTokenPrice - tokenPrice } else { 0L }
202-
(spread, isSorted && spread <= prevSpread)
226+
(spread, isSorted && boxTokenPrice >= tokenPrice && boxDexFeePerToken > 0L && spread <= prevSpread)
203227
})._2
204228
}
205229
}
206230

231+
// counter(buy) orders that are matched against this order
207232
val spendingBuyOrders = INPUTS.filter { (b: Box) =>
208233
b.R4[Coll[Byte]].isDefined && b.R5[Long].isDefined && b.R6[Long].isDefined && {
209234
val buyOrderTokenId = b.R4[Coll[Byte]].get
@@ -213,10 +238,12 @@ private object DexLimitOrderErgoScript {
213238

214239
returnBoxes.size == 1 &&
215240
spendingBuyOrders.size > 0 &&
216-
boxesAreSortedBySpread(spendingBuyOrders) && {
241+
buyOrderBoxesAreSortedBySpread(spendingBuyOrders) && {
217242

218243
val returnBox = returnBoxes(0)
219244

245+
// in case of partial matching new sell order box should be created with tokens that are not matched in this tx
246+
// check that there is only one such box is made later in the code
220247
val foundResidualOrderBoxes = OUTPUTS.filter { (b: Box) =>
221248
val tokenIdParamIsCorrect = b.R4[Coll[Byte]].isDefined && b.R4[Coll[Byte]].get == tokenId
222249
val tokenPriceParamIsCorrect = b.R5[Long].isDefined && b.R5[Long].get == tokenPrice
@@ -229,16 +256,16 @@ private object DexLimitOrderErgoScript {
229256
contractParamsAreCorrect && referenceMe && guardedByTheSameContract
230257
}
231258

259+
// aggregated spread we get from all counter(buy) orders
232260
val fullSpread = { (tokenAmount: Long) =>
233261
spendingBuyOrders.fold((tokenAmount, 0L), { (t: (Long, Long), buyOrder: Box) =>
234262
val returnTokensLeft = t._1
235263
val accumulatedFullSpread = t._2
236264
val buyOrderTokenPrice = buyOrder.R5[Long].get
237265
val buyOrderDexFeePerToken = buyOrder.R6[Long].get
238-
val buyOrderTokenAmount = buyOrder.value / (buyOrderTokenPrice + buyOrderDexFeePerToken)
239-
val priceIsCorrect = buyOrderTokenPrice >= tokenPrice
240-
val tokenAmountInThisOrder = min(returnTokensLeft, buyOrderTokenAmount)
241-
if (spreadIsMine(buyOrder.creationInfo._1) && priceIsCorrect) {
266+
val buyOrderTokenAmountCapacity = buyOrder.value / (buyOrderTokenPrice + buyOrderDexFeePerToken)
267+
val tokenAmountInThisOrder = min(returnTokensLeft, buyOrderTokenAmountCapacity)
268+
if (spreadIsMine(buyOrder.creationInfo._1)) {
242269
// spread is ours
243270
val spreadPerToken = buyOrderTokenPrice - tokenPrice
244271
val buyOrderSpread = spreadPerToken * tokenAmountInThisOrder
@@ -251,25 +278,28 @@ private object DexLimitOrderErgoScript {
251278
})._2
252279
}
253280

281+
// branch for total matching (all tokens are sold and full amount ERGs received)
254282
val totalMatching = (returnBox.value == selfTokenAmount * tokenPrice + fullSpread(selfTokenAmount))
255283

284+
// branch for partial matching, e.g. besides received ERGs we demand a new buy order with tokens for
285+
// non-matched part of this order
256286
val partialMatching = {
257287
foundResidualOrderBoxes.size == 1 && {
258-
val newOrderBox = foundResidualOrderBoxes(0)
259-
val newOrderTokenData = newOrderBox.tokens(0)
260-
val newOrderTokenAmount = newOrderTokenData._2
261-
val soldTokenAmount = selfTokenAmount - newOrderTokenAmount
262-
val minSoldTokenErgValue = soldTokenAmount * tokenPrice
288+
val residualOrderBox = foundResidualOrderBoxes(0)
289+
val residualOrderTokenData = residualOrderBox.tokens(0)
290+
val residualOrderTokenAmount = residualOrderTokenData._2
291+
val soldTokenAmount = selfTokenAmount - residualOrderTokenAmount
292+
val soldTokenErgValue = soldTokenAmount * tokenPrice
263293
val expectedDexFee = dexFeePerToken * soldTokenAmount
264294

265-
val newOrderTokenId = newOrderTokenData._1
266-
val tokenIdIsCorrect = newOrderTokenId == tokenId
295+
val residualOrderTokenId = residualOrderTokenData._1
296+
val tokenIdIsCorrect = residualOrderTokenId == tokenId
267297

268-
val newOrderValueIsCorrect = newOrderBox.value == (SELF.value - expectedDexFee)
269-
val returnBoxValueIsCorrect = returnBox.value == minSoldTokenErgValue + fullSpread(soldTokenAmount)
298+
val residualOrderValueIsCorrect = residualOrderBox.value == (SELF.value - expectedDexFee)
299+
val returnBoxValueIsCorrect = returnBox.value == soldTokenErgValue + fullSpread(soldTokenAmount)
270300
tokenIdIsCorrect &&
271301
soldTokenAmount >= 1 &&
272-
newOrderValueIsCorrect &&
302+
residualOrderValueIsCorrect &&
273303
returnBoxValueIsCorrect
274304
}
275305
}
@@ -379,7 +409,7 @@ object DexLimitOrderContracts {
379409
tokenPrice <- ergoTree.constants.lift(8).collect {
380410
case Values.ConstantNode(value, SLong) => value.asInstanceOf[Long]
381411
}
382-
dexFeePerToken <- ergoTree.constants.lift(20).collect {
412+
dexFeePerToken <- ergoTree.constants.lift(22).collect {
383413
case Values.ConstantNode(value, SLong) =>
384414
value.asInstanceOf[Long]
385415
}
@@ -398,7 +428,7 @@ object DexLimitOrderContracts {
398428
tokenPrice <- ergoTree.constants.lift(9).collect {
399429
case Values.ConstantNode(value, SLong) => value.asInstanceOf[Long]
400430
}
401-
dexFeePerToken <- ergoTree.constants.lift(20).collect {
431+
dexFeePerToken <- ergoTree.constants.lift(22).collect {
402432
case Values.ConstantNode(value, SLong) =>
403433
value.asInstanceOf[Long]
404434
}

0 commit comments

Comments
 (0)