The Design and Regulation of Exchanges A Formal Approach Mohit Garg1and Suneel Sarswat2 1University of Bremen University of Hamburg Germany garguni-bremen.de

2025-04-24 0 0 630.69KB 21 页 10玖币

侵权投诉

The Design and Regulation of Exchanges: A Formal Approach

Mohit Garg1and Suneel Sarswat2

1University of Bremen, University of Hamburg, Germany, garg@uni-bremen.de

2Tata Institute of Fundamental Research, India, suneel.sarswat@gmail.com

October 12, 2022

Abstract

We use formal methods to specify, design, and monitor continuous double auctions, which

are widely used to match buyers and sellers at exchanges of foreign currencies, stocks, and

commodities. We identify three natural properties of such auctions and formally prove that

these properties completely determine the input-output relationship. We then formally verify

that a natural algorithm satisﬁes these properties. All deﬁnitions, theorems, and proofs are

formalized in an interactive theorem prover. We extract a veriﬁed program of our algorithm to

build an automated checker that is guaranteed to detect errors in the trade logs of exchanges if

they generate transactions that violate any of the natural properties.

1 Introduction

Continuous double auctions are widely used to match buyers and sellers at market institutions

such as foreign exchange markets, cryptocurrency exchanges, stock exchanges, and commodities

exchanges. Increasingly, the exchanges deploy automated computer systems for conducting trades,

which often receive a huge number of trade requests, especially in presence of high-frequency algo-

rithmic traders. A minor bug in the computer system of a major exchange can have a catastrophic

eﬀect on the overall economy. To ensure that the exchanges work in a fair and orderly manner,

they are subject to various regulatory guidelines. There have been a number of instances where

the exchanges have been found violating regulatory guidelines [18, 17, 14, 16]. For example, it was

observed that NYSE Arca failed to execute certain trades in violation of the stated rules [18], which

led to the U.S. Securities and Exchange Commission imposing a heavy penalty on the New York

Stock Exchange.

The above example is an instance of a program not meeting its speciﬁcation, where the exchange’s

order matching algorithm is the program and the exchange rules and regulatory guidelines form the

broad speciﬁcations for the program. The reasons for such violations are generally twofold. Firstly,

the exchange rules and the regulatory guidelines are not presented in a formal language; thus, they

tend to be rather vague and ambiguous. Even if they are stated unambiguously, it is not clear

whether they are consistent; they lack a formal proof of consistency. Secondly, the ﬁdelity of the

program implementing the speciﬁcations is traditionally based on repeatedly testing the software

on large data sets and removing all bugs that get detected. Although this approach irons out many

bugs, it is not foolproof; in particular, many bugs that surface only in rare scenarios may easily

remain hidden in the program. A related concern that is often missed is that a faulty program

might continue to make mistakes without anyone noticing or even realizing that they are mistakes.

This is especially relevant in the context of exchanges, where individual traders have a limited view

arXiv:2210.05447v1 [cs.LO] 11 Oct 2022

of the system and may not realize that the exchange is making mistakes, and the regulators might

overlook them, probably because they are not the kinds of mistakes that they look for or are brought

to their notice.

In this work, we introduce a new framework for exchange design and regulation that addresses

the above concerns. We elucidate our approach for an exchange that implements the widely used

continuous double auction mechanism to match buy and sell requests. To this end, we develop the

necessary theoretical results for continuous double auctions which then allows us to apply the formal

methods technology, which has classically been applied to safety-critical systems like nuclear power

plants [21], railway signaling systems, ﬂight control software, and in hardware design (see [19] for a

survey).

More speciﬁcally, we consider a general model for continuous double auctions and identify three

natural properties, namely price-time priority,positive bid-ask spread, and conservation,

that are necessary for any online algorithm implementing continuous double auction to possess.

We then show that any algorithm satisfying these three properties for each input must have a

‘unique’ output at every time step, implying that these three properties are suﬃcient for specifying

continuous double auctions, and there is no need to impose any further requirements on an algorithm

implementing such an auction. We then develop an algorithm and formally prove that it satisﬁes

these three properties. This establishes the consistency of the three properties.

All our proofs are machine-checked; all the notions, deﬁnitions, theorems, and proofs are formal-

ized in the popular Coq proof assistant [15]. Finally, using Coq’s program extraction feature, we

obtain an OCaml program of our veriﬁed algorithm for implementing continuous double auctions.

Such a veriﬁed program is guaranteed to be bug-free and can be directly used at an exchange.

Additionally, enabled by the uniqueness theorem we prove, a veriﬁed program can be used to check

for errors automatically in an existing exchange program by comparing the outputs of the veriﬁed

program against that of the exchange program. Such a veriﬁed checker goes over the trade logs of

the exchange and is guaranteed to detect a violation if the exchange output violates any of the three

properties, and this alleviates the ﬁnal concern we mentioned above. This can be a crucial tool for

regulators. As an application, using our veriﬁed program we check for errors in real data collected

from an exchange.

Thus, our approach can be summed up as follows: The speciﬁcation for an exchange should

consist of a set of provably consistent properties, which are preferably few and simple. Furthermore,

these properties should be rich enough so that one can build an automated checker that can always

detect a violation of the speciﬁcation by going over the logs of the exchange if one exists.

We begin by brieﬂy describing the trading process using continuous double auctions.

1.1 Overview of continuous double auctions

A double auction is a process to match multiple buy and sell orders for a given product at a

marketplace. Potential buyers and sellers of a product place their orders at the market institution

for trade. Buy and sell orders are referred to as bids and asks, respectively. The market institution

on receiving orders is supposed to produce transactions. Each transaction is between a bid and an

ask and consists of a transaction price and a transaction quantity.

More speciﬁcally, each order consists of an order id, timestamp, limit price, and maximum

quantity. Order ids are used to distinguish orders (and hence are unique for each order). Timestamps

represent the arrival times of the orders. For a ﬁxed product, the timestamps of the orders are

distinct.1The limit price of an order ωis the maximum (if ωis a bid) or minimum (if ωis an ask)

possible transaction price for each transaction involving ω. The maximum quantity qof an order ω

is the number of units of the product oﬀered for trade, i.e., the sum of the transaction quantities,

where ωparticipates in, is at most q.

Double auctions are used to generate transactions systematically. There are two common types

of double auctions that are used at various exchanges: call auctions [20, 9, 22] and continuous

double auctions. We discuss call auctions in Section 1.3. In a system implementing continuous

double auctions, buyers and sellers may place their orders at any point in time. On receiving an

order ω, the system instantly tries to match ωwith fully or partially unmatched orders that arrived

earlier (‘resident orders’) and output transactions, before it proceeds to process any other incoming

orders. If there are multiple orders with which ωcan be matched, then the system prioritizes those

matchable orders based on price-time priority (ﬁrst the orders are ranked by the competitiveness

of their price; orders with the same price are then ranked by their arrival time, i.e., as per their

timestamps). If the total transaction quantities of the transactions generated by ωexhaust the

maximum quantity of ω, then it leaves the system completely. Else ωwith its remaining unmatched

quantity is retained by the system for potential future matches; we refer to such unmatched orders

as resident orders. A resident order leaves the system when its quantity gets fully exhausted.

The general model we work with has three primitive instruction types: buy, sell, and delete.2

That is, apart from buy and sell instructions, it is possible to delete a resident order by giving a

‘delete id’ instruction to the system. The system maintains two main logbooks: an order book and a

trade book. The order book is a list of all buy, sell, and delete instructions that the system received,

ordered by their timestamps. The trade book consists of the list of all transactions generated by

the system in the order in which they were generated.

We now describe three natural properties of a system implementing continuous double auctions

that are relevant to our formalization.

•Positive bid-ask spread. This property represents the ‘inertness’ of resident orders; at

any point in time, the resident orders are not matchable to each other, i.e., the limit price

of each resident bid is strictly less than the limit price of each resident ask. This follows

immediately from the fact that an order becomes resident only when it cannot be matched

any further with the existing resident orders (or when there are no matchable resident orders

at all).

•Price-time priority. When a new order arrives, the system tries to match it with the

resident orders and generate transactions. If a less-competitive resident order participates in

one of these transactions, then all current resident orders which are more competitive must

get fully traded in these transactions, where competitiveness is decided based on price-time

priority. This is a direct consequence of the matching process described above.

•Conservation. This property expresses the ‘honesty’ of the system. Roughly speaking, it

states that the system should not lose, create, or modify orders arbitrarily. For example,

when a new incoming order gets partially traded with existing resident orders, it becomes

resident with its maximum quantity precisely being the diﬀerence between its original max-

1In real systems, even if multiple orders arrive at the same time, they are entered into the system one by one.

How this is exactly achieved is beyond the scope of this work.

2In Section 8 we describe how certain other instruction types can be converted to these primitives.

imum quantity and the total quantity of the transactions that are generated. Furthermore,

the timestamp, id, and limit price of the resident order must remain unchanged.

One might feel that many properties would be necessary for specifying ‘conservation’ formally.

On the contrary, later we will see that the above three properties can be stated rather succinctly

once we set up our deﬁnitions appropriately. Also, we will show that any algorithm that implements

these three properties, on any input (order book), will produce a ‘unique’ output at every point in

time, implying that these properties completely characterize continuous double auctions. One can

learn more about double auctions from [5, 12, 3, 4].

1.2 Results

After setting up the deﬁnitions appropriately, we formally represent the three natural properties

of continuous double auctions that we discussed above, namely price-time priority,positive

bid-ask spread, and conservation. We are then able to prove the following results.

•Maximum matching. We ﬁrst show in Lemma 1 that any algorithm that satisﬁes positive

bid-ask spread and conservation, for each incoming order will generate a set of transactions

(‘matching’) whose total quantity will be maximum, i.e., it will be at least the total quantity

of any other feasible set of transactions.

•Local Uniqueness. In Theorem 1 we show that any two processes that satisfy the aforemen-

tioned three properties, for any set of resident orders and an incoming instruction that satisfy

certain technical conditions, will essentially generate the same matching, and the resident

orders that remain at the end of processing this instruction will also be the same. To prove

this theorem we make use of Lemma 1.

•Global Uniqueness. We then show in Theorem 2 that any two processes that satisfy the three

properties, given any order book as input, at any point in time will essentially generate the

same matching, and the resident orders that remain will also be the same. We prove this

theorem by lifting Theorem 1 via an induction argument.

•Correctness of Process_instruction. We then design an algorithm for continuous double auc-

tions which we refer to as Process_instruction and then in Theorem 3 show that it satisﬁes

the three properties.

To use the above results in a practical setting, we extract an OCaml program of our veriﬁed

algorithm Process_instruction, using Coq’s code extraction feature, and then use it to check for

errors in real data from an exchange by running it on order books and then comparing the outputs

with the corresponding trade books. Our global uniqueness theorem implies that if the exchange

program has the three natural properties, then the output of our program should ‘match’ with the

output of the exchange. If they do not match, then at least one of the three properties must be

violated by the exchange program.

Our Coq formalization uses about 6000 lines of new code, which includes about 250 lemmas and

80 deﬁnitions and functions, and is available in the accompanying supplementary materials [1].

1.3 Related work

Mavroudis and Melton [7] study fairness, transparency, and manipulation in exchange systems. They

argue that idealized market models do not capture infrastructural ineﬃciencies and their simple

mechanisms are not robust enough to withstand sophisticated technical manipulation attacks; as

a result, the theoretical fairness guarantees provided by such exchanges are not retained in reality.

To address this problem, they propose the LIBRA system that achieves a relaxed notion of fairness

by making clever use of randomness in routing orders to the matching engine. Our work focuses

on a complementary and an arguably more basic aspect of exchanges; once the system assigns

unique timestamps, even if they are ‘inaccurate’ or ‘unfair’ due to infrastructural inaccuracies or

other reasons, with respect to those timestamps the matching engine should respect the desired

properties; our work focuses on specifying and checking the correctness of the matching engine.

There have been some important works on formalizing ﬁnancial systems, double auctions, and

theorems in economics. We brieﬂy mention a few of them. In an inﬂuential work [11], Passmore

and Ignatovich highlight the need for formal veriﬁcation of ﬁnancial algorithms and suggest various

open problems in the ﬁeld. In response to these challenges, they designed Imandra [10], a special-

ized formal veriﬁcation system and programming language designed to reason about properties of

algorithms that may be proved, refuted, or described.

Cervesato, Khan, Reis, and Žunić [2] present a declarative and modular speciﬁcation for an

automated trading system for continuous double auctions in a concurrent linear framework (CLF)

and implemented it in a CLF type checker that also supports executing of CLF speciﬁcations.

Among other things, they were able to establish that their system is never in a locked or crossed

state, which is equivalent to the positive bid-ask spread property mentioned above.

Wurman, Walsh, and Wellman [20] deal with the theory and implementation of ﬂexible double

auctions for electronic exchanges. In particular, the authors analyze the incentive compatibility of

such auctions. Kaliszyk and Parsert [6] introduce a formal micro-economic framework and formally

prove the ﬁrst welfare theorem leading to a more reﬁned understanding of the theorem than was

available in the economics literature.

Comparison with call auctions. Our work is closely related to the work of Raja, Singh,

and Sarswat [8], which formalizes call auctions. As mentioned earlier, call auctions form a class

of double auctions, which are ‘non-continuous’ or ‘one-shot’ in nature. In call auctions, orders are

collected from buyers and sellers for a ﬁxed duration of time, at the end of which the orders are

matched simultaneously to generate transactions. In [8] call auctions are formalized and certain

uniqueness theorems are obtained. Unlike call auctions, prior to our work, for continuous double

auctions the speciﬁcations were not concisely stated in the literature, hindering formal development

as also noted in [8].

It is interesting to compare call auctions with one time instant of continuous double auctions

when a new order arrives in presence of resident orders. In call auctions two diﬀerent objectives are

usually considered: 1. Maximum matching: produce transactions that maximize the trade volume

(the sum of transaction quantities); 2. Maximum uniform-price matching: produce transactions that

maximize the trade volume subject to the constraint that all the transaction prices are the same.

It turns out, there are instances where meeting these objectives leads to diﬀerent matchings and

trade volumes. In either case, after the transactions are produced, the orders or parts of the order

that remain unmatched are not-matchable, i.e., they have positive bid-ask spread. Compare

this with one time instant of continuous double auction. As we show in this work, positive

bid-ask spread already makes the process unique and can be seen as a special case of a call auction

where the output matching meets both the objectives (1 and 2) simultaneously.3In the context

3For this, we need a slightly relaxed deﬁnition of uniformity: we say a matching has a uniform price if there exists

a common price that can be set for all transactions in the matching such that no limit price of the participating

orders is breached.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

TheDesignandRegulationofExchanges:AFormalApproachMohitGarg1andSuneelSarswat21UniversityofBremen,UniversityofHamburg,Germany,garg@uni-bremen.de2TataInstituteofFundamentalResearch,India,suneel.sarswat@gmail.comOctober12,2022AbstractWeuseformalmethodstospecify,design,andmonitorcontinuousdoubleauctions,...

展开>> 收起<<

The Design and Regulation of Exchanges A Formal Approach Mohit Garg1and Suneel Sarswat2 1University of Bremen University of Hamburg Germany garguni-bremen.de.pdf

共21页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

The Design and Regulation of Exchanges A Formal Approach Mohit Garg1and Suneel Sarswat2 1University of Bremen University of Hamburg Germany garguni-bremen.de

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: