Xác minh chính thức là xác minh một chương trình hoặc thuật toán bằng cách sử dụng một chương trình hoặc thuật toán khác.
Đây là một trong những phương pháp mạnh mẽ nhất cho phép bạn tìm thấy tất cả các lỗ hổng trong chương trình hoặc chứng minh rằng chúng không tồn tại.
Mô tả chi tiết hơn về xác minh hình thức có thể được thấy trong ví dụ giải quyết vấn đề trong bài viết trước của tôi.
Trong bài viết này, tôi chuyển từ xác minh chính thức các vấn đề sang các chương trình và mô tả cách
làm thế nào chúng có thể được chuyển đổi thành hệ thống quy tắc chính thức một cách tự động.
Để làm điều này, tôi đã viết một máy ảo tương tự của riêng mình, sử dụng các nguyên tắc biểu tượng.
Nó phân tích mã chương trình và dịch nó thành một hệ phương trình (SMT), hệ phương trình này có thể được giải bằng chương trình.
Vì thông tin về các phép tính ký hiệu được trình bày trên Internet khá rời rạc,
Tôi sẽ mô tả ngắn gọn nó là gì.
Tính toán ký hiệu là một cách để thực hiện đồng thời một chương trình trên nhiều loại dữ liệu và là công cụ chính để xác minh chương trình chính thức.
Ví dụ: chúng ta có thể đặt điều kiện đầu vào trong đó đối số đầu tiên có thể nhận bất kỳ giá trị dương nào, số âm thứ hai, số 42 thứ ba và đối số đầu ra, ví dụ: XNUMX.
Các phép tính tượng trưng trong một lần chạy sẽ cho chúng ta câu trả lời liệu chúng ta có thể đạt được kết quả mong muốn hay không và một ví dụ về tập hợp các tham số đầu vào như vậy. Hoặc chứng minh rằng không có thông số nào như vậy.
Hơn nữa, chúng ta có thể đặt các đối số đầu vào thành tất cả các đối số có thể và chỉ chọn các đối số đầu ra, chẳng hạn như mật khẩu quản trị viên.
Trong trường hợp này, chúng tôi sẽ tìm thấy tất cả các lỗ hổng của chương trình hoặc lấy bằng chứng cho thấy mật khẩu của quản trị viên là an toàn.
Có thể lưu ý rằng việc thực thi cổ điển của một chương trình với dữ liệu đầu vào cụ thể là một trường hợp đặc biệt của việc thực thi tượng trưng.
Do đó, VM nhân vật của tôi cũng có thể hoạt động ở chế độ mô phỏng của một máy ảo tiêu chuẩn.
Trong phần bình luận của bài viết trước, người ta có thể tìm thấy những lời chỉ trích công bằng về việc xác minh chính thức cùng với việc thảo luận về những điểm yếu của nó.
Các vấn đề chính là:
- Sự bùng nổ tổ hợp, vì việc xác minh chính thức cuối cùng dẫn đến P=NP
- Việc xử lý các cuộc gọi đến hệ thống tệp, mạng và bộ nhớ ngoài khác khó xác minh hơn
- Lỗi trong đặc tả, khi khách hàng hoặc lập trình viên dự định làm một điều gì đó nhưng không mô tả nó đủ chính xác trong đặc tả kỹ thuật.
Do đó, chương trình sẽ được xác minh và tuân thủ các đặc điểm kỹ thuật, nhưng sẽ làm điều gì đó hoàn toàn khác với những gì người sáng tạo mong đợi ở nó.
Vì trong bài viết này, tôi chủ yếu xem xét việc sử dụng xác minh chính thức trong thực tế, nên bây giờ tôi sẽ không đập đầu vào tường và sẽ chọn một hệ thống có độ phức tạp về thuật toán và số lượng lệnh gọi bên ngoài là tối thiểu.
Vì hợp đồng thông minh phù hợp nhất với những yêu cầu này nên lựa chọn rơi vào hợp đồng RIDE từ nền tảng Waves: chúng chưa hoàn thiện Turing và độ phức tạp tối đa của chúng bị giới hạn một cách giả tạo.
Nhưng chúng tôi sẽ xem xét chúng độc quyền từ khía cạnh kỹ thuật.
Ngoài mọi thứ, việc xác minh chính thức sẽ đặc biệt cần thiết đối với bất kỳ hợp đồng nào: thường không thể sửa lỗi hợp đồng sau khi nó đã được đưa ra.
Và chi phí cho những lỗi như vậy có thể rất cao, vì số tiền khá lớn thường được lưu trữ trên các hợp đồng thông minh.
Máy ảo tượng trưng của tôi được viết bằng PHP và Python, đồng thời sử dụng Z3Prover từ Microsoft Research để giải các công thức SMT thu được.
Cốt lõi của nó là tìm kiếm đa giao dịch mạnh mẽ,
cho phép bạn tìm giải pháp hoặc lỗ hổng, ngay cả khi yêu cầu nhiều giao dịch.
Ngay cả , một trong những framework mang tính biểu tượng mạnh mẽ nhất để tìm kiếm các lỗ hổng Ethereum, chỉ mới bổ sung khả năng này vài tháng trước.
Nhưng điều đáng chú ý là các hợp đồng ether phức tạp hơn và Turing hoàn thiện hơn.
PHP dịch mã nguồn của hợp đồng thông minh RIDE thành tập lệnh python, trong đó chương trình được trình bày dưới dạng hệ thống các trạng thái và điều kiện hợp đồng tương thích với Z3 SMT cho quá trình chuyển đổi của chúng:
Bây giờ tôi sẽ mô tả những gì đang xảy ra bên trong chi tiết hơn.
Nhưng trước tiên, hãy nói đôi lời về ngôn ngữ hợp đồng thông minh RIDE.
Nó là một ngôn ngữ lập trình dựa trên chức năng và biểu thức được thiết kế lười biếng.
RIDE chạy độc lập trong blockchain và có thể truy xuất và ghi thông tin từ bộ lưu trữ được liên kết với ví của người dùng.
Bạn có thể đính kèm hợp đồng RIDE vào mỗi ví và kết quả thực hiện sẽ chỉ là TRUE hoặc FALSE.
TRUE có nghĩa là hợp đồng thông minh cho phép giao dịch và FALSE có nghĩa là nó cấm giao dịch.
Một ví dụ đơn giản: tập lệnh có thể cấm chuyển khoản nếu số dư ví nhỏ hơn 100.
Để làm ví dụ, tôi sẽ lấy Sói, Dê và Bắp cải tương tự, nhưng đã được trình bày dưới dạng hợp đồng thông minh.
Người dùng sẽ không thể rút tiền từ ví mà hợp đồng được triển khai cho đến khi anh ta đưa mọi người sang phía bên kia.
#Извлекаем положение всех объектов из блокчейна
let contract = tx.sender
let human= extract(getInteger(contract,"human"))
let wolf= extract(getInteger(contract,"wolf"))
let goat= extract(getInteger(contract,"goat"))
let cabbage= extract(getInteger(contract,"cabbage"))
#Это так называемая дата-транзакция, в которой пользователь присылает новые 4 переменные.
#Контракт разрешит её только в случае если все объекты останутся в сохранности.
match tx {
case t:DataTransaction =>
#Извлекаем будущее положение всех объектов из транзакции
let newHuman= extract(getInteger(t.data,"human"))
let newWolf= extract(getInteger(t.data,"wolf"))
let newGoat= extract(getInteger(t.data,"goat"))
let newCabbage= extract(getInteger(t.data,"cabbage"))
#0 обозначает, что объект на левом берегу, а 1 что на правом
let humanSide= human == 0 || human == 1
let wolfSide= wolf == 0 || wolf == 1
let goatSide= goat == 0 || goat == 1
let cabbageSide= cabbage == 0 || cabbage == 1
let side= humanSide && wolfSide && goatSide && cabbageSide
#Будут разрешены только те транзакции, где с козой никого нет в отсутствии фермера.
let safeAlone= newGoat != newWolf && newGoat != newCabbage
let safe= safeAlone || newGoat == newHuman
let humanTravel= human != newHuman
#Способы путешествия фермера туда и обратно, с кем-то либо в одиночку.
let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage
let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage
let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1
let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage
let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage
let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1
let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage
let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7
#Последняя строка в разделе транзакции описывает разрешающее транзакцию условие.
#Переменные транзакции должны иметь значения 1 или 0, все объекты должны
#быть в безопасности, а фермер должен переплывать реку в одиночку
#или с кем-то на каждом шагу
side && safe && humanTravel && objectTravel
case s:TransferTransaction =>
#Транзакция вывода средств разрешена только в случае если все переплыли на другой берег
human == 1 && wolf == 1 && goat == 1 && cabbage == 1
#Все прочие типы транзакций запрещены
case _ => false
}
Trước tiên, PHP trích xuất tất cả các biến từ hợp đồng thông minh dưới dạng khóa của chúng và biến biểu thức Boolean tương ứng.
cabbage: extract ( getInteger ( contract , "cabbage" ) )
goat: extract ( getInteger ( contract , "goat" ) )
human: extract ( getInteger ( contract , "human" ) )
wolf: extract ( getInteger ( contract , "wolf" ) )
fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1
fState:
wolf:
goat:
cabbage:
cabbageSide: cabbage== 0 || cabbage== 1
human: extract ( getInteger ( contract , "human" ) )
newGoat: extract ( getInteger ( t.data , "goat" ) )
newHuman: extract ( getInteger ( t.data , "human" ) )
goatSide: goat== 0 || goat== 1
humanSide: human== 0 || human== 1
t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage
t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1
t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1
t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage
t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage
t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage
t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage
safeAlone: newGoat != newWolf && newGoat != newCabbage
wolfSide: wolf== 0 || wolf== 1
humanTravel: human != newHuman
side: humanSide && wolfSide && goatSide && cabbageSide
safe: safeAlone || newGoat== newHuman
objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7
PHP sau đó chuyển đổi chúng thành mô tả hệ thống tương thích với Z3Prover SMT bằng Python.
Dữ liệu được gói trong một vòng lặp, trong đó các biến lưu trữ nhận chỉ mục i, biến giao dịch chỉ số i + 1 và các biến có biểu thức đặt quy tắc chuyển từ trạng thái trước sang trạng thái tiếp theo.
Đây chính là trái tim của máy ảo của chúng tôi, nơi cung cấp cơ chế tìm kiếm đa giao dịch.
fState: And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final: fState[Steps]
fState:
wolf:
goat:
cabbage:
cabbageSide: Or( cabbage[i] == 0 , cabbage[i] == 1 )
goatSide: Or( goat[i] == 0 , goat[i] == 1 )
humanSide: Or( human[i] == 0 , human[i] == 1 )
t7: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t3: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] + 1 )
t6: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] - 1 )
t2: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage == cabbage[i] )
t5: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage == cabbage[i] )
t1: And( And( And( humanTravel[i] , wolf == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t4: And( And( And( humanTravel[i] , wolf == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
safeAlone: And( goat[i+1] != wolf , goat[i+1] != cabbage )
wolfSide: Or( wolf[i] == 0 , wolf[i] == 1 )
humanTravel: human[i] != human[i+1]
side: And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] )
safe: Or( safeAlone[i] , goat[i+1] == human[i+1] )
objectTravel: Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] )
data: And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] )
Các điều kiện được sắp xếp và chèn vào mẫu tập lệnh được thiết kế để mô tả hệ thống SMT bằng Python.
Mẫu trống
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
$code$
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
Đối với trạng thái cuối cùng trong toàn bộ chuỗi, các quy tắc được chỉ định trong phần giao dịch chuyển khoản sẽ được áp dụng.
Điều này có nghĩa là Z3Prover sẽ tìm kiếm chính xác các nhóm điều kiện mà cuối cùng sẽ cho phép rút tiền khỏi hợp đồng.
Kết quả là chúng tôi tự động nhận được một mô hình SMT đầy đủ chức năng trong hợp đồng của mình.
Bạn có thể thấy rằng nó rất giống với mô hình trong bài viết trước mà tôi đã biên soạn thủ công.
Mẫu đã hoàn thành
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
human = [ Int('human_%i' % (i + 1)) for i in range(Num) ]
wolf = [ Int('wolf_%i' % (i + 1)) for i in range(Num) ]
goat = [ Int('goat_%i' % (i + 1)) for i in range(Num) ]
cabbage = [ Int('cabbage_%i' % (i + 1)) for i in range(Num) ]
nothing= [ And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] ) for i in range(Num-1) ]
start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ]
safeAlone= [ And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] ) for i in range(Num-1) ]
safe= [ Or( safeAlone[i] , goat[i+1] == human[i+1] ) for i in range(Num-1) ]
humanTravel= [ human[i] != human[i+1] for i in range(Num-1) ]
cabbageSide= [ Or( cabbage[i] == 0 , cabbage[i] == 1 ) for i in range(Num-1) ]
goatSide= [ Or( goat[i] == 0 , goat[i] == 1 ) for i in range(Num-1) ]
humanSide= [ Or( human[i] == 0 , human[i] == 1 ) for i in range(Num-1) ]
t7= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t3= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] + 1 ) for i in range(Num-1) ]
t6= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] - 1 ) for i in range(Num-1) ]
t2= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t5= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t1= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t4= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
wolfSide= [ Or( wolf[i] == 0 , wolf[i] == 1 ) for i in range(Num-1) ]
side= [ And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) for i in range(Num-1) ]
objectTravel= [ Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) for i in range(Num-1) ]
data= [ Or( And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] ) , nothing[i]) for i in range(Num-1) ]
fState= And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final= fState
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
Sau khi ra mắt, Z3Prover giải quyết hợp đồng thông minh và cung cấp cho chúng tôi chuỗi giao dịch cho phép chúng tôi rút tiền:
Winning transaction chain found:
Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0
Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1
Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Transfer transaction
Ngoài hợp đồng phà, bạn có thể thử nghiệm các hợp đồng của riêng mình hoặc thử ví dụ đơn giản này, được giải quyết trong 2 giao dịch.
let contract = tx.sender
let a= extract(getInteger(contract,"a"))
let b= extract(getInteger(contract,"b"))
let c= extract(getInteger(contract,"c"))
let d= extract(getInteger(contract,"d"))
match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,"a"))
let nb= extract(getInteger(t.data,"b"))
let nc= extract(getInteger(t.data,"c"))
let nd= extract(getInteger(t.data,"d"))
nd == 0 || a == 100 - 5
case s:TransferTransaction =>
( a + b - c ) * d == 12
case _ => true
}
Vì đây là phiên bản đầu tiên nên cú pháp rất hạn chế và có thể có lỗi.
Trong các bài viết sau, tôi dự định đề cập đến sự phát triển hơn nữa của VM và chỉ ra cách bạn có thể tạo các hợp đồng thông minh được xác minh chính thức với sự trợ giúp của nó chứ không chỉ giải quyết chúng.
Máy ảo nhân vật có sẵn tại
Sau khi sắp xếp mã nguồn của VM tượng trưng và thêm các nhận xét vào đó, tôi dự định đưa nó lên GitHub để truy cập miễn phí.
Nguồn: www.habr.com