رسمی تصدیق ایک پروگرام یا دوسرے کا استعمال کرتے ہوئے الگورتھم کی تصدیق ہے۔
یہ سب سے طاقتور طریقوں میں سے ایک ہے جو آپ کو پروگرام میں تمام کمزوریوں کو تلاش کرنے یا یہ ثابت کرنے کی اجازت دیتا ہے کہ وہ موجود نہیں ہیں۔
کے مسئلے کو حل کرنے کی مثال میں رسمی تصدیق کی مزید تفصیلی وضاحت دیکھی جا سکتی ہے۔ میرے پچھلے مضمون میں۔
اس مضمون میں میں مسائل کی باضابطہ تصدیق سے پروگراموں کی طرف جاتا ہوں اور اس کا طریقہ بیان کرتا ہوں۔
وہ خود بخود باقاعدہ اصولی نظام میں کیسے تبدیل ہو سکتے ہیں۔
ایسا کرنے کے لیے، میں نے علامتی اصولوں کا استعمال کرتے ہوئے ایک ورچوئل مشین کا اپنا اینالاگ لکھا۔
یہ پروگرام کے کوڈ کو پارس کرتا ہے اور اسے مساوات کے نظام (SMT) میں ترجمہ کرتا ہے، جسے پہلے ہی پروگرام کے ذریعے حل کیا جا سکتا ہے۔
چونکہ علامتی حسابات کے بارے میں معلومات انٹرنیٹ پر پیش کی جاتی ہیں بلکہ ٹکڑے ٹکڑے کر کے،
میں مختصراً بیان کروں گا کہ یہ کیا ہے۔
علامتی حساب کتاب ایک پروگرام کو بیک وقت ڈیٹا کی ایک وسیع رینج پر انجام دینے کا ایک طریقہ ہے اور یہ رسمی پروگرام کی تصدیق کا اہم ذریعہ ہے۔
مثال کے طور پر، ہم ان پٹ کی شرائط سیٹ کر سکتے ہیں جہاں پہلی دلیل کوئی مثبت قدر لے سکتی ہے، دوسری منفی، تیسری صفر، اور آؤٹ پٹ دلیل، مثال کے طور پر، 42۔
ایک رن میں علامتی حسابات ہمیں اس بات کا جواب دیں گے کہ آیا ہمارے لیے مطلوبہ نتیجہ حاصل کرنا ممکن ہے اور اس طرح کے ان پٹ پیرامیٹرز کے سیٹ کی مثال۔ یا اس بات کا ثبوت کہ ایسے کوئی پیرامیٹرز نہیں ہیں۔
مزید یہ کہ، ہم ان پٹ آرگیومینٹس کو تمام ممکنہ دلائل پر سیٹ کر سکتے ہیں، اور صرف آؤٹ پٹ والے کو منتخب کر سکتے ہیں، مثال کے طور پر ایڈمنسٹریٹر پاس ورڈ۔
اس صورت میں، ہم پروگرام کی تمام کمزوریوں کا پتہ لگائیں گے یا ایڈمنسٹریٹر کا پاس ورڈ محفوظ ہونے کا ثبوت حاصل کریں گے۔
یہ نوٹ کیا جاسکتا ہے کہ مخصوص ان پٹ ڈیٹا کے ساتھ کسی پروگرام کا کلاسیکی عمل علامتی عمل درآمد کا ایک خاص معاملہ ہے۔
لہذا، میرا کردار VM معیاری ورچوئل مشین کے ایمولیشن موڈ میں بھی کام کر سکتا ہے۔
پچھلے مضمون کے تبصروں میں کسی کو اس کی کمزوریوں کی بحث کے ساتھ رسمی تصدیق پر منصفانہ تنقید مل سکتی ہے۔
اہم مسائل یہ ہیں:
- مشترکہ دھماکہ، چونکہ رسمی تصدیق بالآخر P=NP پر آتی ہے۔
- فائل سسٹم، نیٹ ورکس اور دیگر بیرونی اسٹوریج پر کالوں کی پروسیسنگ کی تصدیق کرنا زیادہ مشکل ہے۔
- تفصیلات میں کیڑے، جب گاہک یا پروگرامر نے ایک چیز کا ارادہ کیا، لیکن تکنیکی تفصیلات میں اسے کافی حد تک درست طریقے سے بیان نہیں کیا۔
نتیجے کے طور پر، پروگرام کی توثیق کی جائے گی اور تصریح کی تعمیل کی جائے گی، لیکن تخلیق کاروں کو اس سے جو توقع تھی اس سے بالکل مختلف کام کرے گا۔
چونکہ اس مضمون میں میں بنیادی طور پر عملی طور پر تصدیق کے استعمال پر غور کر رہا ہوں، اس لیے میں فی الحال اپنا سر دیوار سے نہیں ٹکاؤں گا، اور ایک ایسے نظام کا انتخاب کروں گا جہاں الگورتھمک پیچیدگی اور بیرونی کالوں کی تعداد کم سے کم ہو۔
چونکہ سمارٹ کنٹریکٹس ان تقاضوں کو بہترین طریقے سے پورا کرتے ہیں، اس لیے انتخاب Waves پلیٹ فارم سے RIDE کنٹریکٹس پر پڑا: وہ ٹورنگ مکمل نہیں ہیں، اور ان کی زیادہ سے زیادہ پیچیدگی مصنوعی طور پر محدود ہے۔
لیکن ہم ان پر خصوصی طور پر تکنیکی پہلو سے غور کریں گے۔
ہر چیز کے علاوہ، رسمی توثیق خاص طور پر کسی بھی معاہدوں کی مانگ میں ہو گی: کسی معاہدے کی غلطی کو شروع کرنے کے بعد اسے درست کرنا عموماً ناممکن ہوتا ہے۔
اور اس طرح کی غلطیوں کی قیمت بہت زیادہ ہو سکتی ہے، کیونکہ کافی بڑی مقدار میں فنڈز اکثر سمارٹ کنٹریکٹس پر محفوظ کیے جاتے ہیں۔
میری علامتی ورچوئل مشین PHP اور Python میں لکھی گئی ہے، اور نتیجے میں SMT فارمولوں کو حل کرنے کے لیے Microsoft ریسرچ سے Z3Prover استعمال کرتی ہے۔
اس کے مرکز میں ایک طاقتور کثیر لین دین کی تلاش ہے، جو
آپ کو حل یا کمزوریاں تلاش کرنے کی اجازت دیتا ہے، چاہے اس کے لیے بہت سے لین دین کی ضرورت ہو۔
یہاں تک کہ Ethereum کی کمزوریوں کو تلاش کرنے کے لیے سب سے طاقتور علامتی فریم ورک میں سے ایک، صرف چند ماہ قبل اس صلاحیت کو شامل کیا گیا تھا۔
لیکن یہ بات قابل غور ہے کہ ایتھر معاہدے زیادہ پیچیدہ اور ٹورنگ مکمل ہیں۔
پی ایچ پی RIDE سمارٹ کنٹریکٹ کے سورس کوڈ کا ایک ازگر اسکرپٹ میں ترجمہ کرتا ہے، جس میں پروگرام کو Z3 SMT کے موافق نظام کے طور پر پیش کیا جاتا ہے کنٹریکٹ سٹیٹس اور ان کی ٹرانزیشن کی شرائط:
اب میں مزید تفصیل سے بیان کروں گا کہ اندر کیا ہو رہا ہے۔
لیکن پہلے، RIDE سمارٹ کنٹریکٹ کی زبان کے بارے میں چند الفاظ۔
یہ ایک فعال اور اظہار پر مبنی پروگرامنگ زبان ہے جو ڈیزائن کے لحاظ سے سست ہے۔
RIDE بلاکچین کے اندر تنہائی میں چلتی ہے اور صارف کے بٹوے سے منسلک اسٹوریج سے معلومات کو بازیافت اور لکھ سکتی ہے۔
آپ ہر پرس کے ساتھ RIDE کا معاہدہ منسلک کر سکتے ہیں، اور اس پر عمل درآمد کا نتیجہ صرف صحیح یا غلط ہوگا۔
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
}
پی ایچ پی سب سے پہلے سمارٹ کنٹریکٹ سے تمام متغیرات کو ان کی کیز اور متعلقہ بولین ایکسپریشن متغیر کی شکل میں نکالتا ہے۔
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
پی ایچ پی پھر انہیں 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 کے سورس کوڈ کو ترتیب میں رکھنے اور وہاں تبصرے شامل کرنے کے بعد، میں اسے مفت رسائی کے لیے GitHub پر پوسٹ کرنے کا ارادہ رکھتا ہوں۔
ماخذ: www.habr.com