처음부터 공식 검증 시스템을 만듭니다. 1부: PHP 및 Python의 문자 가상 머신

공식 검증은 다른 프로그램이나 알고리즘을 사용하여 검증하는 것입니다.

이는 프로그램의 모든 취약점을 찾거나 존재하지 않음을 증명할 수 있는 가장 강력한 방법 중 하나입니다.

형식 검증에 대한 자세한 설명은 문제 해결의 예에서 볼 수 있습니다. 늑대와 염소와 양배추 내 이전 기사에서.

이 기사에서는 문제의 공식 검증에서 프로그램으로 이동하고 방법을 설명합니다.
어떻게 자동으로 공식 규칙 시스템으로 변환할 수 있습니까?

이를 위해 나는 상징적 원리를 사용하여 가상 머신의 아날로그를 직접 작성했습니다.

이는 프로그램 코드를 구문 분석하여 이미 프로그래밍 방식으로 풀 수 있는 방정식 시스템(SMT)으로 변환합니다.

기호계산에 관한 정보는 인터넷상에 다소 단편적으로 제시되어 있기 때문에,
그것이 무엇인지 간략하게 설명하겠습니다.

기호계산은 광범위한 데이터에 대해 프로그램을 동시에 실행하는 방법으로, 공식적인 프로그램 검증을 위한 주요 도구입니다.

예를 들어, 첫 번째 인수가 양수 값, 두 번째 음수, 세 번째 42, 출력 인수(예: XNUMX)를 취할 수 있는 입력 조건을 설정할 수 있습니다.

한 번의 실행으로 기호 계산을 수행하면 원하는 결과를 얻을 수 있는지 여부에 대한 답과 이러한 입력 매개변수 집합의 예를 얻을 수 있습니다. 또는 그러한 매개변수가 없다는 증거입니다.

또한 입력 인수를 가능한 모든 인수로 설정하고 출력 인수(예: 관리자 비밀번호)만 선택할 수 있습니다.

이 경우 프로그램의 모든 취약점을 찾아내거나 관리자의 비밀번호가 안전하다는 증거를 확보하게 됩니다.

특정 입력 데이터를 가진 프로그램의 고전적인 실행은 기호 실행의 특별한 경우라는 점을 알 수 있습니다.

따라서 내 캐릭터 VM은 표준 가상 머신의 에뮬레이션 모드에서도 작동할 수 있습니다.

이전 기사에 대한 논평에서 공식적인 검증의 약점에 대한 논의와 함께 공정한 비판을 찾을 수 있습니다.

주요 문제는 다음과 같습니다.

1. 공식 검증이 궁극적으로 P=NP로 귀결되므로 조합 폭발
2. 파일 시스템, 네트워크 및 기타 외부 저장소에 대한 호출 처리를 확인하기가 더 어렵습니다.
3. 고객이나 프로그래머가 한 가지를 의도했지만 기술 사양에서 이를 충분히 정확하게 설명하지 않은 경우 사양의 버그입니다.

결과적으로 프로그램은 사양을 검증하고 준수하지만 제작자가 기대했던 것과는 완전히 다른 작업을 수행하게 됩니다.

이 기사에서는 실제로 형식 검증의 사용을 주로 고려하므로 지금은 벽에 부딪치지 않고 알고리즘의 복잡성과 외부 호출 수가 최소화되는 시스템을 선택하겠습니다.

스마트 계약은 이러한 요구 사항에 가장 적합하기 때문에 Waves 플랫폼의 RIDE 계약을 선택했습니다. 이는 Turing 완전하지 않으며 최대 복잡성이 인위적으로 제한됩니다.

그러나 우리는 기술적 측면에서만 이를 고려할 것입니다.

모든 것 외에도 모든 계약에 대해 공식적인 검증이 특히 요구됩니다. 일반적으로 계약이 시작된 후에는 계약 오류를 수정하는 것이 불가능합니다.
그리고 그러한 오류로 인한 비용은 매우 높을 수 있습니다. 왜냐하면 꽤 많은 양의 자금이 스마트 계약에 저장되는 경우가 많기 때문입니다.

내 기호 가상 머신은 PHP와 Python으로 작성되었으며 Microsoft Research의 Z3Prover를 사용하여 결과 SMT 공식을 해결합니다.

그 핵심에는 강력한 다중 트랜잭션 검색이 있습니다.
많은 트랜잭션이 필요한 경우에도 솔루션이나 취약점을 찾을 수 있습니다.
조차 미스릴Ethereum 취약점을 찾기 위한 가장 강력한 상징적 프레임워크 중 하나인 는 몇 달 전에야 이 기능을 추가했습니다.

그러나 에테르 계약이 더 복잡하고 튜링 완전하다는 점은 주목할 가치가 있습니다.

PHP는 RIDE 스마트 계약의 소스 코드를 Python 스크립트로 변환합니다. 여기서 프로그램은 계약 상태 및 전환 조건에 대한 Z3 SMT 호환 시스템으로 표시됩니다.

이제 내부에서 일어나는 일을 더 자세히 설명하겠습니다.

하지만 먼저 RIDE 스마트 계약 언어에 대해 몇 마디 말씀드리겠습니다.

설계상 게으른 기능적 표현 기반 프로그래밍 언어입니다.
RIDE는 블록체인 내에서 독립적으로 실행되며 사용자의 지갑에 연결된 저장소에서 정보를 검색하고 쓸 수 있습니다.

각 지갑에 RIDE 계약을 첨부할 수 있으며, 실행 결과는 TRUE 또는 FALSE로만 표시됩니다.

TRUE는 스마트 계약이 거래를 허용한다는 것을 의미하고, FALSE는 거래를 금지한다는 것을 의미합니다.
간단한 예: 지갑 잔액이 100 미만인 경우 스크립트는 이체를 금지할 수 있습니다.

예를 들어, 동일한 늑대, 염소, 양배추를 사용하지만 이미 스마트 계약의 형태로 제시되어 있습니다.

사용자는 모든 사람을 상대방에게 보낼 때까지 계약이 배포된 지갑에서 돈을 인출할 수 없습니다.

#Извлекаем положение всех объектов из блокчейна
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

}

PHP는 먼저 키와 해당 부울 표현식 변수의 형태로 스마트 계약에서 모든 변수를 추출합니다.

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는 이를 Python의 Z3Prover SMT 호환 시스템 설명으로 변환합니다.
데이터는 스토리지 변수가 인덱스 i, 트랜잭션 변수 인덱스 i + 1을 수신하고 표현식이 있는 변수가 이전 상태에서 다음 상태로 전환하기 위한 규칙을 설정하는 루프로 래핑됩니다.

이것이 다중 트랜잭션 검색 엔진을 제공하는 가상 머신의 핵심입니다.

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] )  

조건은 정렬되어 Python의 SMT 시스템을 설명하도록 설계된 스크립트 템플릿에 삽입됩니다.

빈 템플릿

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()
 

전체 체인의 마지막 상태에 대해서는 전송 트랜잭션 섹션에 지정된 규칙이 적용됩니다.

이는 Z3Prover가 궁극적으로 계약에서 자금을 인출할 수 있는 조건 세트를 정확하게 찾을 것임을 의미합니다.

결과적으로 우리는 계약의 완전한 기능을 갖춘 SMT 모델을 자동으로 받게 됩니다.
내가 수동으로 컴파일한 이전 기사의 모델과 매우 유사하다는 것을 알 수 있습니다.

완성된 템플릿

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()
 

출시 후 Z3Prover는 스마트 계약을 해결하고 자금을 인출할 수 있는 일련의 거래를 제공합니다.

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

페리 계약 외에도 자신만의 계약을 실험하거나 2번의 트랜잭션으로 해결되는 간단한 예를 시도해 볼 수 있습니다.

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

}

첫 번째 버전이다 보니 구문이 매우 제한되어 있고 버그가 있을 수 있습니다.
다음 기사에서는 VM의 추가 개발에 대해 다루고 VM의 도움을 받아 단순히 문제를 해결하는 것이 아니라 공식적으로 검증된 스마트 계약을 생성하는 방법을 보여줄 계획입니다.

캐릭터 가상머신은 다음에서 이용 가능합니다. http://2.59.42.98/hyperbox/
심볼릭 VM의 소스코드를 정리하고 거기에 코멘트를 추가한 후 GitHub에 올려 무료로 접근할 예정입니다.

출처 : habr.com