VeriSolid: Correct-by-Design Smart Contracts for Ethereum

Vanderbilt University & University of Houston & Aristotle University of Thessaloniki

FC, 2018

基於區塊鏈的分散式賬本的採用正在快速增長，因為它們能夠在沒有可信實體的情況下提供可靠性，完整性和可審計性。這些新興平臺的關鍵功能之一是能夠建立自我執行的智慧合約。然而，事實證明，智慧合約的開發在實踐中容易出錯，因此，部署在公共平臺上的合同常常充滿安全漏洞。這些平臺的設計加劇了這個問題，這些平臺禁止更新合同程式碼並回滾惡意交易。鑑於此，在部署智慧合約並使用大量加密貨幣信任它之前確保智慧合約是安全的至關重要。為此，我們引入了VeriSolid框架，用於使用具有嚴格操作語義的基於轉換系統的模型指定的合同的形式驗證。我們基於模型的方法允許開發人員在高抽象級別上推理和驗證合同行為。 VeriSolid允許從經過驗證的模型生成Solidity程式碼，從而實現智慧合約的正確設計開發。

An Empirical Study of Speculative Concurrency in Ethereum Smart Contracts

我們使用歷史資料來估計並行執行以太坊智慧合約的投機技術的潛在好處。 我們使用簡單的推測執行引擎，隨著時間的推移重放以太坊區塊鏈中的取樣塊的事務跟蹤。 在此引擎中，礦工嘗試並行執行塊中的所有事務，並回滾導致資料衝突的事務。 然後順序執行中止的事務。 驗證員執行與礦工相同的計劃。 我們發現，我們的投機技術產生的估計加速在2016年約為8倍，在2017年底下降至約2倍，其中加速是使用天然氣成本或指令計數來衡量的。 我們還觀察到一小部分合同導致由推測性併發執行導致的許多資料衝突.

Communication cost of consensus for nodes with limited memory

CMU & Google & ETH Zurich & UCB

受區塊鏈和感測器網路中的應用的啟發，我們考慮n個節點的模型試圖在其多數位上達成共識。每個節點i在零時刻被分配一個位，並且是具有m位儲存器（即，2m狀態）和泊松時鐘的有限自動機。當i的時鐘響起時，我可以選擇進行通訊，然後匹配到統一選擇的節點j。節點j和i可以基於另一節點的狀態更新它們的狀態。以前的工作重點是儘量縮短達成共識的時間和錯誤的可能性，而我們的目標是最大限度地減少通訊次數。我們證明當m> 3 log log log（n）時，可以以線性通訊成本達到一致，但是如果m <log log log（n）則這是不可能的。我們還研究了模型的同步變體，其中用於實現線性通訊成本的m的上限和下限分別是2log log log（n）和log log log（n）。關鍵步驟是區分節點何時可以意識到知道多數位並停止通訊。我們表明，如果他們的記憶太低，這是不可能的.

Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins

University of Cambridge

2018年的前六個月，加密貨幣盜竊案達到7.61億美元，該技術也是最新和最好的洗錢工具。 犯罪率的上升使研究人員和執法部門都在尋找追蹤犯罪所得的方法。 雖然跟蹤演算法最近有所改進，但它們仍然會產生大量資料，其中很少有資料點與調查人員相關或感興趣，更不用說普通比特幣所有者對起源感興趣了。 在這項工作中，我們描述了在區塊鏈上視覺化相關資料的努力。 為了實現這一目標，我們提出了一個圖形模型來表示被盜硬幣，然後使用各種視覺化技術實現這一點。

Superlight – A Permissionless, Light-client Only Blockchain with Self-Contained Proofs and BLS Signatures

University of Applied Sciences Rapperswil, Rapperswil, Switzerland

-Blockchain協議基於分散式公共資料庫，其中保證儲存的資料是不可變的。所有節點都必須維護自己相同的本地資料庫副本的要求可確保安全性，而共識機制有助於確定將哪些資料新增到資料庫並防止強大的攻擊者使系統脫軌。但是，由於構成區塊鏈基礎的資料庫是不斷增長的塊列表，因此可伸縮性是該技術的固有問題。一些公共區塊鏈需要幾百GB到幾TB的儲存空間。在這項工作中，我們提出了具有自包含證明的Superlight概念，旨在提高區塊鏈協議的可擴充套件性，同時保持安全性和分散性。節點可以通過僅使用鏈的塊頭來匯出事務的有效性，而不是所有節點都具有整個區塊鏈的本地副本來驗證事務。為了使塊頭保持緊湊，BLS簽名用於組合簽名。我們提供SCP的正式定義，並顯示客戶端建立其他節點接受的證據所需的步驟。這種輕客戶端區塊鏈協議的優點是儲存要求較低，但缺點是由於BLS簽名導致計算複雜性增加，由於缺乏全域性狀態而導致用例有限，以及傳送方之間需要互動協議，接收者和礦工來建立交易。

Energy Crowdsourcing and Peer-to-Peer Energy Trading in Blockchain-Enabled Smart Grids

The University of Texas at San Antonio & Southern Methodist University & Siemens Corporate Technology & Washington State University

電網正在迅速轉型，雖然最近的電網創新提高了先進控制方法的利用率，但下一代電網需要能夠整合分散式能源（DER）的技術 - 以及無縫購買和銷售電力的消費者。本文開發了一個優化模型和基於區塊鏈的架構來管理眾包能源系統（CES）的運作，以及點對點（P2P）能源交易交易。考慮到各種型別的能源交易交易和眾包，提出了分銷網路中CES的運營模型。然後，提出了兩階段運算演算法：階段I側重於發電和可控DER的日前排程，而階段II則針對配電網路的提前或實時執行而開發。所開發的方法支援各個專業消費者和/或公用事業之間的P2P能量交易。所提出的操作模型也可用於操作孤島微電網。然後通過有效的區塊鏈實現（即IBM Hyperledger Fabric）對CES框架和操作演算法進行原型化。該實現允許系統運營商管理網路使用者以無縫地交換能量。提供了案例研究和原型圖。