Как выполнить формальную проверку в смарт-контрактах C# Stratis

Задний план

Кажется, почти каждую неделю мы слышим об ошибках и инцидентах безопасности, связанных со смарт-контрактами, которые приводят к значительным финансовым и репутационным потерям для организаций и частных лиц.

Смарт-контракты содержат реализации DAO, систем голосования, токенов, NFT, сервисов DeFi и многих других видов приложений и активов блокчейна.

По своей природе смарт-контракты могут быть доступны любому, их код может быть проверен кем угодно, а их транзакции и изменения состояния записываются в общедоступную цепочку блоков и могут наблюдаться кем угодно.

== Соедините эти факты с неизменностью транзакций смарт-контрактов, и вы получите заманчивую цель для преднамеренных эксплойтов злоумышленников и источник потенциально катастрофических последствий от непреднамеренных ошибок программирования в коде смарт-контракта.==

Не менее 50 лет поле формальной проверки предложил программистам заманчивое видение устранения ошибок программирования и автоматического поиска ошибок и уязвимостей в операционных системах и приложениях с использованием формальной логики и математики.

Формальная верификация относится к процессу автоматической проверки аппаратной или программной системы на наличие ошибок путем проверки формальной модели системы на соответствие формальным требованиям или спецификациям поведения.

И модели, и спецификации достаточно точны, чтобы компьютер мог выполнять проверки с помощью таких инструментов, как автоматические средства доказательства теорем и решатели SMT.

Могут использоваться различные формальные модели, например. цифровая электронная или механическая система может быть смоделирована как конечный автомат, а формальная спецификация может быть списком действительных переходов состояний для системы.

Формальная проверка показала бы, что система никогда не совершает переходы между состояниями, кроме тех, что указаны в спецификации, без необходимости тщательного тестирования и наблюдения каждого возможного состояния разработчиком или программистом.

Таким образом, формальная верификация является своего рода [статическим анализом] (https://en.wikipedia.org/wiki/Static_program_analysis), когда предпринимается попытка вывести свойства программы путем изучения ее исходного кода или двоичного кода без фактического выполнения кода. программа.

Статический анализ программы можно противопоставить таким методам, как модульное тестирование и фаззинг, которые являются формами [динамического анализа программы] (https://en.wikipedia.org/wiki/Dynamic_program_analysis). Динамический анализ зависит от программиста и приложения для тестирования или фаззинга, определяющего условия, при которых программный код будет выполняться и проверяться, например, диапазон входных значений для метода смарт-контракта.

Однако программы и среда, в которой они выполняются, часто бывают достаточно сложными, поэтому программистам практически невозможно заранее указать или смоделировать все входные данные или условия, с которыми столкнется программа, и в целом изучить поведение, возникающее в результате каждого условия.

Эксплойты в смарт-контрактах обычно возникают из-за того, что злоумышленники обнаруживают поведение программы из-за определенных очень специфических входных данных смарт-контракта, а также пограничных случаев и состояний блокчейна, которые заранее не учитывались программистами.

Сегодня многие области вычислительной техники, такие как промышленные и критически важные для безопасности системы, разработка микропроцессоров, разработка и реализация криптографических протоколов, реализация драйверов устройств операционной системы и другие, зависят от формальной проверки и широко используют ее.

Такие проекты, как seL4 и CertiKOS (разработано некоторыми из основателей [CertiK] (https://www.certik.com/)) показали, что осуществима формальная верификация сложных программ, таких как целые ядра операционных систем.

В настоящее время существует множество инструментов и языков программирования для проведения формальной проверки программного обеспечения либо для существующих языков, таких как C, Java или Solidity, либо с помощью совершенно новых языков, которые напрямую поддерживают построение формальных спецификаций.

Хотя формальную проверку может быть сложно реализовать для приложений общего назначения, смарт-контракты очень хорошо подходят для формальных проверка в связи с требованиями:

• Детерминизм

• Ограниченное выполнение и изменение состояния

• Простота логики

• Конечное время выполнения

В блокчейне разные узлы должны иметь возможность достигать консенсуса по изменениям состояния блокчейна путем добавления транзакций. Поэтому смарт-контракты не должны содержать такие операции, как ввод-вывод и сетевые вызовы или вызовы даты и времени, или любые операции, которые могут выполняться по-разному из-за различий в аппаратных или программных средах разных узлов блокчейна.

Сюда входят операции, которые динамически выделяют память в куче, что может привести к сбою из-за нехватки памяти. Смарт-контракты используют явное понятие состояния в отличие от обычных программ, где состояние определяется только неявно, а такие вещи, как изменяемые глобальные переменные, изменяемые общедоступные поля или произвольные объекты, размещенные в куче, обычно не разрешены в смарт-контрактах.

Единственный способ постоянно делиться или сохранять состояние в методах смарт-контрактов — это использовать хранилище состояний в блокчейне. Эти характеристики упрощают различение чистых функций, которые не оказывают побочных эффектов на видимое состояние программы (например, средства получения свойств C#), что упрощает формальную проверку.

Логика программы смарт-контрактов должна быть простой и не запутанной, чтобы ее можно было легко понять и проверить. Наконец, смарт-контрактам выделяется конечное количество газа, что гарантирует остановку выполнения после конечного количества инструкций, поэтому такие вещи, как бесконечные циклы, невозможны.

Все эти характеристики делают программы смарт-контрактов очень удобными для формальной проверки. Хотя модульное и комплексное тестирование, тестирование черного ящика, фаззинг и другие способы динамического анализа и тестирования смарт-контрактов всегда будут важны, формальная проверка смарт-контрактов предлагает способ значительно повысить безопасность и правильность смарт-контрактов.

Несколько компаний, таких как CertiK, предлагают коммерческие услуги для проверки смарт-контрактов с использованием собственной технологии формальной проверки, и существует множество инструментов с открытым исходным кодом с различными подходами к формальной проверке. проверка смарт-контрактов.

Подходы к формальной проверке смарт-контрактов в Ethereum

Существует несколько инструментов с открытым исходным кодом для статического анализа смарт-контрактов Ethereum, включая Модуль компилятора языка Solidity SMTChecker, который может формально проверять функцию контракта предварительные условия, утверждения и инварианты контракта. как и другие условия, такие как наличие арифметического переполнения и доступ к массиву за пределами границ.

Существуют также внешние [формальные инструменты проверки] (https://github.com/leonardoalt/ethereum_formal_verification_overview#smart-contracts), такие как [Act] (https://github.com/ethereum/act), язык для написания формальных спецификаций. для смарт-контрактов Ethereum. Такие компании, как CertiK, проводят исследования в области формальной проверки с помощью новых языков, таких как [DeepSEA] (https://www.certik.com/resources/blog/technology/an-introduction-to-deepsea#home), которые можно скомпилировать в байт-код EVM. Эти три инструмента представляют собой 3 разных подхода к проверке смарт-контрактов Ethereum.

SMTChecker компилятора Solidity пытается статически проверить предварительные условия метода и утверждает в коде Solidity, что означает, что вам не нужно изучать другой язык или инструмент, например.

```javascript

// Идентификатор лицензии SPDX: GPL-3.0

прочность прагмы >=0,8,0;

контракт Макс {

функция max(uint[] memory _a) public pure возвращает (uint) {

требуют (_a.length >= 5);

инт м = 0;

for (uint i = 0; i < _a.length; ++i)

если (_a[i] > m)

м = _а[я];

for (uint i = 0; i < _a.length; ++i)

утверждать (м > _a [я]);

вернуть м;

является примером проверяемого метода в Solidity с использованием существующих функций проверки во время выполнения «assert» и «require». При использовании SMTChecker requires объявляет предварительное условие, которое является условием, включающим параметры функции, которые должны быть статически проверены, прежде чем функция будет вызвана другими функциями.

При таком подходе спецификации контрактов выводятся и проверяются непосредственно из кода Solidity без необходимости использования другого языка или инструмента.

[Act] (https://github.com/ethereum/act), с другой стороны, — это совершенно отдельный язык, который используется для объявления формальной спецификации смарт-контракта Ethereum, например.

```javascript

конструктор StateMachine

конструктор интерфейса()

создает

uint256 х := 0

инварианты

х <= 1

поведение f StateMachine

интерфейс f()

случай х == 0:

место хранения

х => 1

гарантирует

(пост(х) == 0) или (пост(х) == 1)

поведение g StateMachine

интерфейс г()

случай х == 1:

место хранения

х => 0

гарантирует

(пост(х) == 1) или (пост(х) == 0)

пример формальной спецификации в Act для простого контракта Solidity ниже:

```javascript

контракт StateMachine {

х;

функция f () общедоступная {

если (х == 0)

х = 1;

функция g() общедоступная {

если (х == 1)

х = 0;

Такие компании, как Runtime Verification, также используют формальные языки и платформы с открытым исходным кодом, такие как K, для разработки формальных спецификаций для смарт-контрактов EVM и Ethereum, внешних по отношению к коду Solidity.

Ключом к этому подходу является использование языка, отдельного от языка реализации, для объявления формальной спецификации смарт-контракта.

DeepSEA — это также совершенно отдельный от Solidity язык с синтаксисом, напоминающим функциональные языки, такие как OCaml.

Однако в DeepSEA вы пишете как спецификацию смарт-контракта, так и реализацию на одном языке, например.

```javascript

константа _totalSupply = 100000

подпись объекта ERC20Interface = {

конструктор: модуль -> модуль;

const totalSupply : unit -> int;

const balanceOf : адрес -> int;

передача: адрес * int -> bool;

одобрить: адрес * int -> bool;

TransferFrom : адрес * адрес * int -> bool

объект FixedSupplyToken : ERC20Interface {

пусть балансы: отображение [адрес] int: = mapping_init

пусть допуски: отображение [адрес] отображение [адрес] int: = mapping_init

пусть конструктор () =

балансы [msg_sender] := 100000

пусть totalSupply () =

пусть bal0 = балансы [адрес (0)] в

_totalSupply — bal0

пусть балансOf tokenOwner =

пусть bal = балансы[tokenOwner] в

бал

пусть перевод (toA, токены) =

пусть fromA = msg_sender в

пусть from_bal = балансы[fromA] в

пусть to_bal = балансирует[toA] в

assert(fromA<>toA/\from_bal>= токены);

балансы[отA] := from_bal-токены;

балансы[toA] := to_bal+токены;

истинный

Компилятор DeepSEA генерирует как исполняемый байт-код, который может работать на EVM, так и официальную спецификацию, которая может быть прочитана и доказана в интерактивном режиме с помощью средства доказательства теорем Кока.

Ключевым моментом, который следует учитывать при таком подходе, является то, что реализация и спецификация смарт-контрактов выполняются на одном языке, хотя это язык, с которым программисты Solidity вряд ли знакомы.

Формальная проверка смарт-контракта в Stratis

Silver – это инструмент с открытым исходным кодом для статического анализа и формальной проверки Stratis смарт-контрактов C#.

Silver использует платформу Spec#, разработанную Microsoft Research для разработки формально проверенных объектно-ориентированных программ на C#.

Spec# основывается на идее спецификации программы, выраженной непосредственно в коде C# с использованием некоторых небольших расширений языка C#, компилятора, который может понимать эти расширения, и средства проверки программы (под кодовым названием Boogie, позже выделенного как независимый проект), который статически проверяет соответствие байт-кода CIL, сгенерированного компилятором Spec#, спецификации программы.

![Из «Проверки программы с использованием системы программирования Spec#» Розмари Манохан] (https://cdn.hackernoon.com/images/byyBIeQCMgdx887WlsJiWCUFDr22-h4c3ha6.png)

Spec# максимально использует C#, предоставляя при этом некоторые новые ключевые слова и конструкции, которые позволяют программисту выражать контракты методов и классов в виде предварительных условий, постусловий, утверждений, инвариантов цикла и инвариантов класса, используя логические квантификаторы, такие как forall и exists и простые математические функции, такие как max и min.

Silver использует обновленную версию Spec# и поддерживает совместимость с существующими компиляторами C#, позволяя встраивать спецификации Spec# в виде комментариев при переписывании кода C# с помощью переписчиков синтаксиса Roslyn для обеспечения совместимости со старым диалектом C# 2.0, который понимает Spec#.

Когда вы компилируете смарт-контракт C# с помощью Silver с помощью флага --verify или используете команду verify, Silver переписывает ваш код и создает другую сборку, скомпилированную с помощью компилятора Spec#. Код в этой сборке .NET содержит метаданные, позволяющие преобразовать его в Boogie и официально проверить верификатором программы Boogie. Вы можете встраивать аннотации Spec# в свой код C# в виде комментариев, которые переписываются и считываются компилятором Spec# как формальная спецификация для вашего смарт-контракта.

Ключевая особенность подхода Spec# к формальной проверке и то, что делает его таким привлекательным, заключается в том, что спецификации записываются непосредственно в код смарт-контракта с использованием синтаксиса C#. Spec# сохраняет преимущества того, что язык спецификации совпадает с языком реализации, но при этом позволяет писать и проверять широкий и мощный набор ограничений спецификации, используя знакомый синтаксис C#. Таким образом, серебро — это формальный инструмент проверки, который сочетает в себе некоторые преимущества различных подходов к проверке смарт-контрактов Ethereum, которые мы видели ранее.

Мы собираемся продублировать некоторые примеры формальной проверки, которые мы рассмотрели перед использованием C#, чтобы дать вам представление о том, как использовать Silver. Мы создадим Visual Studio пример проекта с именем SimpleVerabilityContracts для хранения кода нашего контракта. Вы можете загрузить [выпуск] уровня Silver (https://github.com/allisterb/Silver/releases) или собрать его самостоятельно, следуя инструкциям в [репозитории] GitHub (https://github.com/allisterb/Silver#building). ).

Контракты методов

Во-первых, давайте рассмотрим пример функции «Max» из документации Solidity SMTChecker. Имейте в виду, что языки смарт-контрактов, как правило, не содержат встроенных или библиотечных функций, которые делают такие вещи, как сортировка, потому что эти функции потребляют много газа и в большинстве случаев лучше подходят для работы вне сети с помощью подключенного dApp.

Но в некоторых случаях такие функции могут быть необходимы, поэтому мы можем наивно реализовать функцию Max в качестве примера проверяемого метода контракта C#. Наша C#-версия Max выглядит так:

```csharp

частный uint Max(uint[] a)

//@ требуется a.Length >= 5;

//@ гарантирует forall{int i in (0:a.Length); результат >= а[я]};

инт м = 0;

for (int n = 0; n < a.Length; n++)

//@ инвариант forall {int i in (0:n); м >= а[я]};

если (а [п] > м)

м = а[п];

вернуть м;

Код почти такой же, как и у функции Solidity, но короче. Код Spec#, объявляющий спецификацию метода, встроен в виде комментариев, которые сохраняют совместимость с другими компиляторами C# и Stratis [инструмент проверки SCT] (https://github.com/stratisproject/Stratis.SmartContracts.Tools.Sct).

Вы используете ключевое слово requires для указания предварительных условий метода, ключевое слово ensures для указания постусловий метода, ключевое слово invariant для указания инвариантов цикла и квантификатор forall для утверждения условий или предикатов, которые истинны для всех значений в множество. Мы можем проверить этот проект смарт-контракта в командной строке с помощью Silver CLI:

``PowerShell

примеры компиляции серебра\SimpleVerifiedContractsSimpleVerifiedContracts.csproj --verify

-c Арифметика

Silver переписывает наш код для использования компилятором Spec#, компилирует и проверяет его. Опция -c фильтрует выходные данные верификатора, сопоставляя только имена классов с этим именем. Мы получаем следующий вывод:

Любой код, который не соответствует спецификации нашего контракта, будет помечен верификатором Silver, например, если в нашем методе CallMax мы передаем массив из 4 чисел в наш метод Max, это не будет проверять:

Утверждения

Для обработки произвольных длин массивов в публичных методах нам нужно использовать функцию ==runtime== Assert из API смарт-контрактов Stratis:

общедоступный uint Max(uint[] a)

```csharp

общедоступный uint Max (uint [] a)

//@ требуется a.Length >= 5;

//@ гарантирует forall{int i in (0:a.Length); результат >= а[я]};

Assert(a.Length >= 5, "Длина массива должна быть больше 5.");

инт м = 0;

for (int n = 0; n < a.Length; n++)

//@ инвариант forall {int i in (0:n); м >= а[я]};

если (а [п] > м)

м = а[п];

вернуть м;

Если Max будет методом публичного контракта, а не просто библиотечным методом, функция ==runtime== Assert должна использоваться для обработки массивов произвольной длины, потому что у компилятора Spec# нет возможности проверить значения параметров в среды выполнения, которые передаются методу виртуальной машиной Stratis CLR.

A ==runtime== Assert немедленно выйдет из метода, если условие или предикат не выполнены, поэтому из логического POV мы знаем, что любой код с этого момента будет иметь это условие.

Таким образом, во время выполнения «Assert» в методе преобразуется в ключевое слово «предполагать» в Spec#... логически мы можем предположить, что «a.Length >= 5» в любой точке метода после времени выполнения «Assert», пока значение не может изменить снова.

==Static== assertы и инварианты в Spec#, с другой стороны, действуют как контрольные точки для верификатора. A ==static== assert говорит, что указанное условие должно быть истинным в этой точке программы, и верификатор программы попытается доказать, что утвержденное условие выполняется.

Есть много случаев, когда вы должны статически утверждать условия, чтобы заставить верификатор продолжить проверку некоторого окончательного свойства или условия... чем больше статических утверждений вы используете в своем коде, тем больше вы помогаете верификатору программы. (Убедитесь, что вы понимаете разницу между ==runtime== with-the-capital-A Assert и ==static== with-the-common-a assert.)

Очень распространенный тип статического утверждения, который вы будете часто использовать, — это инварианты цикла.

Инварианты цикла

Инварианты цикла задают условия, которые всегда будут выполняться при выполнении цикла C#. Инварианты циклов имеют решающее значение для того, чтобы Spec# мог проверять код, содержащий циклы, такие как блоки for и while, и хотя Spec# может выводить некоторые из них автоматически, почти всегда необходимо явно указать некоторые в вашем коде. Например, если мы удалим инвариант цикла в приведенном выше коде, превратив его в обычный комментарий:

// инвариант forall {int i in (0:n); м >= а[я]};

Spec# не может проверить выполнение постусловия:

```sql

Результаты проверки

└── Файл: c:\Projects\Silver\examples\SimpleVerifiedContracts\bin\Debug
etcoreapp3.1\ssc\SimpleVerifiedContracts.dll

└── Методы

├── ArithmeticContract..ctor$Stratis.SmartContracts.ISmartContractState$notnull: Ok

│ └── Продолжительность: 0,322931 с

├── ArithmeticContract.Max$System.UInt32.array$notnull: Ошибка

│ ├── Ошибки

│ │ └── Метод ArithmeticContract.Max(uint[]! a), невыполненное постусловие: forall{int i in (0:a.Length); результат >= а[я]}

│ │ └── Файл:

│ └── Продолжительность: 0,0190016 с

└── ArithmeticContract.CallMax: Ошибка

├── Ошибки

│ └── Вызов ArithmeticContract.Max(uint[]! a), невыполненное предварительное условие: a.Length >= 5

│ ├── Файл: c:\Projects\Silver\examples\SimpleVerifiedContracts\ssc\Arithmetic.cs

│ ├── Строка: 26

│ └── Колонка: 9

└── Продолжительность: 0,024215 с

[09:48:29 INF] 2 из 7 методов не прошли проверку.

Давайте рассмотрим еще один пример C# с использованием инвариантов цикла, на этот раз из языка DeepSEA. У DeepSEA пока не так много примеров использования, но в папке unittests репозитория есть несколько примеров, которые мы можем посмотреть. , как функция умножения, реализованная в виде цикла for:

```цельc

пусть _val : int := 0

( a может быть отрицательным; b должно быть положительным )

пусть умножить (a, b) =

для i = 0 сделать b

начинать

пусть val = _val в

_знач := значение + а

конец;

пусть val = _val в assert(val = a*b);

_val := 0

Это просто умножение, реализованное как цикл for, добавляющий a к себе b раз. Мы можем реализовать это на C# следующим образом:

```csharp

частный uint Multiply (uint a, uint b)

//@ гарантирует результат == a * b;

уинт знач = 0;

для (uint i = 0; i < b; i++)

//@ инвариант i <= b;

//@ инвариант val == a * i;

вал += а;

возвращаемое значение;

Несмотря на то, что это чрезвычайно простая функция, я допустил ошибки при ее реализации в первый раз. Я использовал условие цикла i <= b вместо i < b, и верификатор поймал его:

```sql

Результаты проверки

└── Файл: c:\Projects\Silver\examples\SimpleVerifiedContracts\bin\Debug
etcoreapp3.1\ssc\SimpleVerifiedContracts.dll

└── Методы

├── ArithmeticContract..ctor$Stratis.SmartContracts.ISmartContractState$notnull: Ok

│ └── Продолжительность: 0,3247862 с

├── ArithmeticContract.Max$System.UInt32.array$notnull: Хорошо

│ └── Продолжительность: 0,0189602 с

├── ArithmeticContract.CallMax: Хорошо

│ └── Продолжительность: 0,0329967 с

└── ArithmeticContract.Multiply$System.Int32$System.UInt32: Ошибка

├── Ошибки

│ └── После итерации цикла: инвариант цикла может не выполняться: i <= b

│ ├── Файл: c:\Projects\Silver\examples\SimpleVerifiedContracts\ssc\Arithmetic.cs

│ ├── Строка: 73

│ └── Колонка: 20

└── Продолжительность: 0,0090002 с

[10:24:28 INF] 1 из 8 методов не прошел проверку.

Оба инварианта снова необходимы для проверки выполнения постусловия.

Проверка методов контракта C# с состоянием

Оба примера, которые мы рассмотрели до сих пор, являются примерами чистых функций. В программировании чистый обычно обозначает функции или методы, которые не изменяют видимое состояние программы или объекта при выполнении; алгоритмы для числовых операций являются типичными примерами чистых функций.

Существует более сильная версия pure, которая обозначает функции, возвращаемое значение которых зависит только от значений параметров, таких как математические функции, то есть функции, которые являются детерминированными, но более слабая версия чаще используется в объектно-ориентированном программировании и именно ее использует Spec#.

Смарт-контракты обычно включают изменение состояния блокчейна путем добавления блоков, содержащих созданные ими транзакции. Итак, давайте рассмотрим пример метода контракта, который приводит к изменению состояния блокчейна.

Представьте, что мы хотим создать приложение Stratis DeFi, которое помогает людям делать пожертвования их любимому разработчику с открытым исходным кодом. Реализация смарт-контракта на C# может начинаться примерно так:

```csharp

использование Stratis.SmartContracts;

открытый класс DonateContract : SmartContract

публичный DonateContract (состояние ISmartContractState)

: база (состояние)

state.PersistentState.SetAddress(имя(владелец), state.Message.Sender);

публичная пустота Donate ()

Передача(Владелец, Сообщение.Значение);

частный владелец адреса

получить => вернуть State.GetAddress (имя (владелец));

set => State.SetAddress (имя (владелец), значение);

Это очень простой контракт, который берет все, что CRS отправляется на него, и `Передает адрес владельца. Владелец смарт-контракта хранится в постоянном состоянии в конструкторе, и этот код запускается один раз при создании контракта. Итак, как мы можем официально проверить этот контракт?

Нам нужно написать спецификацию, которой всегда должно соответствовать поведение метода Donate. Давайте представим, что есть метод GetBalance(Address address), который возвращает баланс CRS для произвольного адреса блокчейна Stratis.

Этот метод не существует в смарт-контрактах Stratis для произвольных адресов, и в большинстве блокчейнов эту функцию нетривиально реализовать... но на уровне спецификации все, что нас интересует, это то, как эта функция ведет себя, а не ее реализация.

==При написании спецификаций важно помнить, что нужно сосредоточиться на логике, а не на реализации.==

Если бы у нас был такой метод, мы могли бы сказать, что после завершения метода «Перевод» значение «GetBalance(Owner)» должно быть равно старому значению «GetBalance(Owner)» + все, что было отправлено в сообщении смарт-контракту, т.е.

```csharp

ulong oldBalance = Получить Баланс (Владелец); // Получить старый баланс для адреса владельца

Передача(Владелец, Сообщение.Значение); // Передаем все, что было отправлено

assert GetBalance(Owner) == oldBalance + Message.Value; //Новый баланс теперь должен включать все, что было отправлено.

Это наша первая попытка спецификации. Чтобы написать это в Spec#, нам просто нужно добавить 3 аннотации к нашему смарт-контракту:

```csharp

использование Stratis.SmartContracts;

открытый класс DonateContract : SmartContract

публичный DonateContract (состояние ISmartContractState)

: база (состояние)

state.PersistentState.SetAddress(имя(владелец), state.Message.Sender);

публичная пустота Donate ()

//@ предположим Microsoft.Contracts.Owner.None(Owner);

//@ ulong oldBalance = GetBalance(Owner);

Передача(Владелец, Сообщение.Значение);

//@ assert GetBalance(Owner) == oldBalance + Message.Value;

частный владелец адреса

получить => вернуть State.GetAddress (имя (владелец));

set => State.SetAddress (имя (владелец), значение);

Первое, что бросается в глаза, — это аннотация со ссылкой на Microsoft.Contracts.Owner. Причина, по которой это необходимо, заключается в том, что Owner — это свойство класса SmartContract, то есть вызов метода, а не поле. В Spec# есть идея изменчивости объекта, когда вызов метода переключает получателя (цель) метода в изменяемое или «не принадлежащее» состояние, когда у него нет «владельца», и каждый другой объект в вызове, который может быть изменен, должен находиться в одном и том же изменяемом состоянии.

Это происходит автоматически для полей, но не для свойств. Это всего лишь небольшая бухгалтерская деталь при написании спецификаций, в которых используются свойства вместо полей, и сейчас это не важно.

Важными частями нашей спецификации являются строки выше и ниже нашего вызова метода Transfer, где мы объявляем переменную с именем oldBalance, а затем говорим, что баланс адреса владельца равен oldBalance плюс значение все, что было отправлено в сообщении.

Метод GetBalance, который мы видим выше, является частью Silver [базовой библиотеки смарт-контрактов] (https://github.com/allisterb/Silver/tree/master/src/Stratis.SmartContracts) и не является частью API Stratis. для смарт-контрактов. Доступ к нему возможен только в спецификации, то есть внутри блоков операторов //@.

Но... когда мы пытаемся это проверить, это не проходит:

О-о, похоже, мы ошиблись в своих рассуждениях.

Когда мы [смотрим] (https://github.com/stratisproject/Stratis.SmartContracts/blob/e91521b829f2aaa5d85407dc613b05451c8a1158/Stratis.SmartContracts/SmartContract.cs#L65), мы видим, что метод Transfer фактически возвращает ITransferResult, который указывает на успех или неудачу операции передачи. По логике вещей, баланс адреса владельца будет увеличиваться только в случае успеха ITransferResult. Таким образом, мы можем сказать это в нашей спецификации для нашего метода Donate:

```csharp

публичная пустота Donate ()

//@ предположим Microsoft.Contracts.Owner.None(Owner);

//@ ulong oldBalance = GetBalance(Owner);

ITransferResult r = Transfer(Владелец, Сообщение.Значение);

//@ утверждать r.Success ==> GetBalance(Owner) == oldBalance + Message.Value;

где ==> — оператор логического следствия в Spec#. С этой спецификацией метод Donate успешно проверен:

```sql

[11:03:08 INF] Компиляция прошла успешно с 0 предупреждениями. Сборка находится по адресу c:\Projects\Silver\examples\SimpleVerifiedContracts\bin

\Debug
etcoreapp3.1\ssc\SimpleVerifiedContracts.dll.

Результаты проверки

└── Файл: c:\Projects\Silver\examples\SimpleVerifiedContracts\bin\Debug
etcoreapp3.1\ssc\SimpleVerifiedContracts.dll

└── Методы

├── ArithmeticContract..ctor$Stratis.SmartContracts.ISmartContractState$notnull: Ok

│ └── Продолжительность: 0,2784462 с

├── ArithmeticContract.Max$System.UInt32.array$notnull: Хорошо

│ └── Продолжительность: 0,0190412 с

├── ArithmeticContract.CallMax: Хорошо

│ └── Продолжительность: 0,034999 с

├── ArithmeticContract.Multiply$System.Int32$System.UInt32: Хорошо

│ └── Длительность: 0,0079999 с

├── DonateContract..ctor$Stratis.SmartContracts.ISmartContractState$notnull: Хорошо

│ └── Продолжительность: 0,1226313 с

├── DonateContract.Donate: Хорошо

│ └── Продолжительность: 0,086572 с

├── DonateContract.get_Owner: Хорошо

│ └── Продолжительность: 0,0195311 с

└── DonateContract.set_Owner$Stratis.SmartContracts.Address$notnull: Хорошо

└── Продолжительность: 0,0155473 с

[11:03:10 INF] Проверка прошла успешно для 8 методов.

Получив правильную спецификацию, мы можем написать окончание assert в качестве пост-условия для метода Donate, превратив это статическое assert в Assert во время выполнения и заменив переменную oldBalance с помощью Spec# старый оператор. Окончательная версия нашего простого проверяемого метода "Пожертвовать":

```sql

публичная пустота Donate ()

//@ гарантирует GetBalance(Owner) == old(GetBalance(Owner)) + Message.Value;

//@ предположим Microsoft.Contracts.Owner.None(Owner);

ITransferResult r = Transfer(Владелец, Сообщение.Значение);

Assert(r.Success, "Передача не удалась." );

Анализ

Конечно, мы могли бы найти проблему в нашем коде, написав модульный тест и используя фиктивную структуру, которая имитировала бы ITransferResult, не возвращая Success. Но разница в том, что с помощью формальной проверки мы нашли ошибку в нашем коде. путем сверки формальной спецификации метода с его реализацией, и эта же процедура найдет все ошибки в коде, не соответствующие спецификации.

Наша процедура поиска ошибок опирается на логику и написание единой спецификации, а не на нашу способность предвидеть и писать тесты для каждого условия, которое может возникнуть, когда наш код взаимодействует с окружающей средой. Хотя для написания формальной спецификации требуется еще несколько строк кода, спецификации в Spec# кратки и непрерывны с нашим существующим кодом C#, в отличие от таких языков, как Act или K framework.

Заключение

Надеюсь, эта статья дала вам небольшое представление о том, что такое формальная проверка и как она может помочь вам разработать более безопасные смарт-контракты. Даже при написании очень простого кода, такого как метод «Умножить» или «Пожертвовать», мне нравилось ощущение, что проверяющий смотрит через мое плечо и указывает на возможные ошибки. Обычные ошибки программирования, такие как ошибки условий цикла, могут потенциально привести к катастрофическим последствиям в смарт-контрактах.

Одним из способов сравнения формальной проверки с другими методами анализа и тестирования является наблюдение за тем, что динамический анализ, такой как модульные тесты и тестирование черного ящика, обычно дает недооценку и ложноотрицательные результаты в отношении потенциальных проблем безопасности в коде смарт-контракта, в то время как методы статического анализа, такие как формальная проверка, обычно производят завышенная оценка и ложные срабатывания в отношении потенциальных проблем.

Серебро в настоящее время находится в разработке, и есть много способов улучшить формальные функции проверки, например, прямо сейчас серебро не дает никаких указаний, почему условие или инвариант не выполняются. Должна быть возможность извлечь эту информацию из модели Z3, которая была сгенерирована как контрпример, чтобы показать, что условия проверки недействительны. Кроме того, использование Silver из интерфейса командной строки не является оптимальным, было бы гораздо лучше, если бы эта информация была доступна внутри Visual Studio через существующий [Silver Roslyn анализатор] (https://www.nuget.org/packages/Silver. Анализ кода/).

Мы только коснулись этой огромной темы, и эта статья является лишь первой из, надеюсь, многих других статей о формальной проверке смарт-контрактов Stratis C# как отличного способа дополнить существующие методы динамического анализа и тестирования, а также повысить безопасность блокчейна. приложения и активы.