Now 5515 visitors
Today:0 Yesterday:0
Total: 148247
212S 50P 4R
2026-10-20, Week 43 |
| Member Login |
| TACT Journal Homepage |
| Call for Paper |
| Committee |
| Find My Paper |
| Author Homepage |
| Statistics & History |
| Welcome Message |
| Paper Procedure |
| FAQ |
| Paper Archives |
| Outstanding Papers |
| Author Homepage |
| - Paper Procedure |
| - Journal Procedure |
| - Presentation Tips |
|
| Program & Proceedings |
| Program with Papers |
| Plenary Session |
| Tutorial Session |
|
| Presentation Platform |
| Hotel & Travel Info |
| About Korea |
| Accommodation |
| Transportation |
| VISA |
| Other Infomation |
|
| Photo Gallery |
| Scheduler Login |
| Seminar |
| Archives Login |
|
| Sponsors |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
 ICACT20210216 Slide.01
[Big Slide]
[YouTube] |
Chrome  Click!! |
 |
Hello. I’m Woong Sub Park, a mater’s course in Korea University’s School of Cybersecurity.
My presentation topic is Formal Modeling of Smart Contract-based Trading System.
|
| ICACT20210216 Slide.02
[Big Slide]
|
Chrome Click!! |
 |
The table of contents is as follows.
First, Blockchain,
Second, Smart Contract,
Third, Formal methods,
Fourth, Model Checking and UPPAAL modeling tool briefly explain.
Then, Fifth, Formal Modeling using UPPAAL
Finally, let me tell you about a conclusion.
|
| ICACT20210216 Slide.03
[Big Slide]
|
Chrome Click!! |
 |
Blockchain is decentralized distributed ledger technology.
The main features are Immutability, transparency, and trustlessness.Therefore, blockchain attracts attention as a technology that enables secure transactions by storing and operating trusted assets (e.g., cryptocurrency, stock ledger, insurance ledger, real estate contract, electronic ballot paper, intellectual property rights, etc.)
|
| ICACT20210216 Slide.04
[Big Slide]
|
Chrome Click!! |
 |
In, 2013, ethereum was proposed by Vitalik Buterin.
Ethereum is a platform for developing decentralized applications (DApps) based on blockchain technology.
On Ethereum, you can send a bunch ether into a computer program and once you've done this, the computer program (itself) has the ability to control where the money goes.
As a representative service of Ethereum, it has the advantage of being able to implement programs written in Solidity as smart contract functions.
|
| ICACT20210216 Slide.05
[Big Slide]
|
Chrome Click!! |
 |
Smart contract, which was first proposed as a concept in 1994 by Nick Szabo, has developed into an environment suitable for practical use with the development of blockchain technology.
In other words, it has increased the possibility of digitally automating the way humans fulfilled terms of contracts, which are traditionally written in writing.
Smart contracts are computer code running on the blockchain according to certain rules and are contracts that are automatically executed when predefined rules are met. Smart contracts provide advantages such as clarity, predictability, surveillance, and ease of execution in contractual relationships.
Therefore, transactions can be made without intermediaries within the blockchain network even with non-trusted parties.
Initial blockchains could only execute smart contracts written for specific domains, but since the advent of Ethereum, various smart contracts can be converted digitally.
Accordingly, various attempts are being made to convert the terms of execution of contracts specified in the existing written form into smart contracts through appropriate analysis in various fields.
|
| ICACT20210216 Slide.06
[Big Slide]
|
Chrome Click!! |
 |
As the blockchain technology develops, the field of application of smart contracts has expanded.
However, if there is a problem with the security vulnerability of the smart contract and the contradictions and errors of the smart contract itself, it has a characteristic that cannot be corrected once it is deployed, which can lead to a fatal accident soon.
One of the most well-known cases of damage, DAO ATTACK, one of the functions of DAO was to participate in crowdsale of investors and get Ether refunded. During the process of this function, there was a flaw in the logic of coding.
Therefore, it was a case in which 3.6 million ETH was stolen by repeatedly requesting a refund. In addition, there are PARITY WALLET hacking and SMART MESH hacking.
Therefore, in this paper, we intend to verify the smart contract through formal modeling, one of the formal specifications, before deploying the smart contract.
|
| ICACT20210216 Slide.07
[Big Slide]
|
Chrome Click!! |
 |
Errors may exist in various stages of the development process and errors become more expensive as they move through the software development lifecycle, and it’s more cost effective to fix bugs earlier than later.
So, a formal methods are needed.
Formal methods are various mathmetical techniques used for the formal specification and development of software.
Formal specification is usually used in requirement and design phase as formal requirements specification, formal design specification.
Given such a specification, it is possible to use formal verification techniques to demonstrate that a system design is correct with respect to its specification.
Formal specifications describe what a system should do.
Generally adds robustness to software and increased confidence in its correctness.
Safety critical area is one domain to which mathematical techniques have been successfully applied.
Likewise, Smart Contract is Finance Critical system.
Therefore, in the early stages of smart contract development, errors and contradictions must be corrected through formal methods.
|
| ICACT20210216 Slide.08
[Big Slide]
|
Chrome Click!! |
 |
Model checking is a type of formal method, which is an automated technique that shows whether the properties of such a model are satisfied for a given system's finite state model and logical properties.
As shown in Figure 4, Model checking consists of a model that specifies the system, specific properties of the system, and a model checker that operates by receiving properties and models.
In order to do model checking, first, finite state-based modeling is performed and specific properties of the model are specified using Temporal Logic. The specified model and properties are verified using the model checker to verify that the model satisfies the properties. Model checker is fully automated and generates counterexamples through error tracking.
UPPAAL is an integrated tool environment for modeling, validation and verificaction of real-time systems modeled as networks of timed automata.
Network means, system is modelled as a network several timed automata in parallel. |
| ICACT20210216 Slide.09
[Big Slide]
|
Chrome Click!! |
 |
Smart contracts can be used in industries related to finance, insurance, trading, auctions, public documentation, and services, etc, as shown in Figure 5.
This paper formal modeling an auction system based on smart contracts related to trading.
Of the many auction systems I have modeled open descending auctions and these auctions are used by Google and IPOs, etc.
Public descending auctions are also referred to as Netherlands auctions, and this auction system is an auction method in which the seller's offer price decreases over time, unlike traditional auction systems.
The seller can set the lowest proposed price before the auction begins, and the price of the item cannot be lower than the lowest proposed price when the auction is in progress.
The buyer can bid on the item if he believes it is the right price to buy the item, and if the bid is the first bid, the transaction is closed and the auction ends. |
| ICACT20210216 Slide.10
[Big Slide]
|
Chrome Click!! |
 |
The above model is a model of a Beneficiary(seller) of a smart contract-based Dutch auction system using the UPPAAL modeling tool.
First, the seller sets the auction time, the initial proposed price of the item, the lowest proposed price, the deduction amount, and the deduction time interval and distributes the smart contract.
At this time, if you enter an incorrect value, the deployment is terminated because it is an invalid smart contract.
Also, if the auction ends correctly, the contract will be terminated and it will return to the waiting state for deployment.
And, Deadlock does not occur due to time constraints in all states, and the auction ends automatically when the auction end time specified by the seller is reached. |
| ICACT20210216 Slide.11
[Big Slide]
|
Chrome Click!! |
 |
The above model is a model of a Bidder(buyer) of a smart contract-based Dutch auction system using the UPPAAL modeling tool.
First, the buyer can see that when the beneficiary(seller) deploys the contract, the bidder(buyer) can simultaneously confirm that it is deployed through the ‘broadcast channel’.
After that, randomly decides whether to participate in the auction in these model.
If another model does not participate in the auction, it will transition to the end state.
If you want to participate in an auction, you will randomly decide the quantity and price you want to buy.
And you can keep checking the current price in ‘check price’ state, and if the price you want to buy matches the current price, you can bid.
At this time, two bidders are not allowed, the product and amount are delivered and the auction ends. |
| ICACT20210216 Slide.12
[Big Slide]
|
Chrome Click!! |
 |
The above model is a model of a Contract of a smart contract-based Dutch auction system using the UPPAAL modeling tool.
When the beneficiary(seller) deploys the contract in the 'inactive' state(initial state), the contract transitions into the 'active' state.
And the deduction amount is reduced from the initial proposed price in the deduction time interval set by the beneficiary(seller).
In the 'active' state, the contract transitions into an inactive state if the beneficiary(seller) has set an incorrect input value or the auction ends correctly. |
| ICACT20210216 Slide.13
[Big Slide]
|
Chrome Click!! |
 |
TCTL is a mechanism that can express constant boundaries for delays between state transitions to model finite-state systems, and which is accepted by UPPAAL.
E in TCTL means ‘exists a path’ in tree logic, and it is expressed as E in UPPAAL.
A in TCTL means ‘for all path’ in tree logic, and it is expressed as A in UPPAAL.
G in TCTL means ‘all states in a path’ in tree logic, and it is expressed as [] in UPPAAL.
F in TCTL means ‘some state in a path’ in tree logic, and it is expressed as <> in UPPAAL. |
| ICACT20210216 Slide.14
[Big Slide]
|
Chrome Click!! |
 |
The properties derived from the functional requirements of the smart contract were converted to TCTL.
Property 1 states that if the deduction time interval specified by the beneficiary and the clock of the contract template becomes the same, the current proposed price is the same as the price reduced by the deduction amount from the initial proposed price.
In this property, the 'count' variable represents the number of times the amount has been decreased. And when the clock of the contract template becomes equal to the deduction time interval, it is initialized to 0.
Property 2 states that if the bidder in the bidding state is bidder(i) and bidder(j), it means that i and j are the same, indicating that it cannot exist in the bidding state at the same time.
property 3 is a safety property, and it has been shown that the initial proposed price does not deducted below the lowest proposed price in all states of all routes. |
| ICACT20210216 Slide.15
[Big Slide]
|
Chrome Click!! |
 |
And, property 4 is a safety property.
It means that the bid is delivered to the beneficiary. At this time, in the above property, it was assumed that the beneficiary initial asset is 0.
property 5 is the liveness property, indicating that the contract will be terminated someday when the contract is deployed.
The UPPAAL model checker was used to confirm that the model satisfies the above properties derived from the functional requirements |
| ICACT20210216 Slide.16
[Big Slide]
|
Chrome Click!! |
 |
Smart contracts are finance critical systems.
Therefore, it is very important to detect errors and inconsistencies before deploy.
These characteristics can be guaranteed through formal method.
Therefore, we modeled and verified that the model satisfies the functional requirements properties of smart contract through formal modeling, one of the formal method.
In future research, we plan to implement these models using ‘Solidity’ language and check whether the implemented smart contract satisfies the functional requirements.
|
| ICACT20210216 Slide.17
[Big Slide]
|
Chrome Click!! |
 |
If you have any questions about this presentation, please contact me by email below.
Thank you for watching my presentation.
|
| |
