การตรวจสอบอย่างเป็นทางการคือการตรวจสอบโปรแกรมหรืออัลกอริทึมหนึ่งโดยใช้อีกโปรแกรมหนึ่ง
นี่เป็นหนึ่งในวิธีการที่ทรงพลังที่สุดที่ช่วยให้คุณสามารถค้นหาช่องโหว่ทั้งหมดในโปรแกรมหรือพิสูจน์ได้ว่าไม่มีอยู่จริง
คำอธิบายโดยละเอียดเพิ่มเติมของการตรวจสอบอย่างเป็นทางการสามารถดูได้ในตัวอย่างการแก้ปัญหาของ ในบทความก่อนหน้าของฉัน
ในบทความนี้ ฉันย้ายจากการตรวจสอบปัญหาอย่างเป็นทางการไปยังโปรแกรมและอธิบายวิธีการ
พวกมันจะถูกแปลงเป็นระบบกฎที่เป็นทางการโดยอัตโนมัติได้อย่างไร
ในการทำเช่นนี้ ฉันเขียนอะนาล็อกของเครื่องเสมือนของตัวเองโดยใช้หลักการเชิงสัญลักษณ์
แยกวิเคราะห์โค้ดโปรแกรมและแปลเป็นระบบสมการ (SMT) ซึ่งสามารถแก้ไขได้โดยทางโปรแกรมแล้ว
เนื่องจากข้อมูลเกี่ยวกับการคำนวณเชิงสัญลักษณ์ถูกนำเสนอบนอินเทอร์เน็ตค่อนข้างไม่เป็นชิ้นเป็นอัน
ฉันจะอธิบายสั้น ๆ ว่ามันคืออะไร
การคำนวณเชิงสัญลักษณ์เป็นวิธีการรันโปรแกรมบนข้อมูลที่หลากหลายไปพร้อมๆ กัน และเป็นเครื่องมือหลักสำหรับการตรวจสอบโปรแกรมอย่างเป็นทางการ
ตัวอย่างเช่น เราสามารถกำหนดเงื่อนไขอินพุตโดยที่อาร์กิวเมนต์แรกสามารถรับค่าบวก ค่าลบที่สอง ศูนย์ที่สาม และอาร์กิวเมนต์เอาต์พุต เช่น 42
การคำนวณเชิงสัญลักษณ์ในการรันครั้งเดียวจะให้คำตอบว่าเป็นไปได้หรือไม่ที่เราจะได้รับผลลัพธ์ที่ต้องการและตัวอย่างชุดของพารามิเตอร์อินพุตดังกล่าว หรือพิสูจน์ว่าไม่มีพารามิเตอร์ดังกล่าว
ยิ่งไปกว่านั้น เราสามารถตั้งค่าอาร์กิวเมนต์อินพุตให้กับอาร์กิวเมนต์ที่เป็นไปได้ทั้งหมด และเลือกเฉพาะเอาต์พุต เช่น รหัสผ่านผู้ดูแลระบบ
ในกรณีนี้ เราจะค้นหาช่องโหว่ทั้งหมดของโปรแกรมหรือรับการพิสูจน์ว่ารหัสผ่านของผู้ดูแลระบบนั้นปลอดภัย
สังเกตได้ว่าการดำเนินการแบบคลาสสิกของโปรแกรมที่มีข้อมูลอินพุตเฉพาะเป็นกรณีพิเศษของการดำเนินการเชิงสัญลักษณ์
ดังนั้นตัวละครของฉัน VM ยังสามารถทำงานในโหมดจำลองของเครื่องเสมือนมาตรฐานได้
ในความคิดเห็นต่อบทความก่อนหน้านี้ เราจะพบคำวิจารณ์ที่ยุติธรรมเกี่ยวกับการตรวจสอบอย่างเป็นทางการพร้อมทั้งการอภิปรายถึงจุดอ่อนของมัน
ปัญหาหลักคือ:
- การระเบิดแบบผสมผสาน เนื่องจากการตรวจสอบอย่างเป็นทางการท้ายที่สุดลงมาที่ P=NP
- การประมวลผลการเรียกไปยังระบบไฟล์ เครือข่าย และพื้นที่จัดเก็บข้อมูลภายนอกอื่นๆ ยากต่อการตรวจสอบ
- จุดบกพร่องในข้อกำหนด เมื่อลูกค้าหรือโปรแกรมเมอร์มีจุดประสงค์อย่างใดอย่างหนึ่ง แต่ไม่ได้อธิบายอย่างถูกต้องเพียงพอในข้อกำหนดทางเทคนิค
เป็นผลให้โปรแกรมได้รับการตรวจสอบและปฏิบัติตามข้อกำหนด แต่จะทำสิ่งที่แตกต่างไปจากที่ผู้สร้างคาดหวังโดยสิ้นเชิง
เนื่องจากในบทความนี้ ฉันกำลังพิจารณาการใช้การตรวจสอบอย่างเป็นทางการเป็นหลักในทางปฏิบัติ ฉันจะไม่เอาหัวโขกกำแพงในตอนนี้ และจะเลือกระบบที่ความซับซ้อนของอัลกอริทึมและจำนวนการโทรจากภายนอกมีน้อย
เนื่องจากสัญญาอัจฉริยะเหมาะสมกับข้อกำหนดเหล่านี้มากที่สุด ตัวเลือกจึงตกอยู่กับสัญญา RIDE จากแพลตฟอร์ม Waves: สัญญาเหล่านี้ยังไม่สมบูรณ์ของทัวริง และความซับซ้อนสูงสุดถูกจำกัดอย่างเกินจริง
แต่เราจะพิจารณาจากด้านเทคนิคโดยเฉพาะ
นอกเหนือจากทุกสิ่งทุกอย่างแล้ว การตรวจสอบอย่างเป็นทางการจะต้องมีสัญญาใดๆ เป็นพิเศษ โดยปกติแล้วจะเป็นไปไม่ได้ที่จะแก้ไขข้อผิดพลาดของสัญญาหลังจากที่เปิดตัวแล้ว
และค่าใช้จ่ายของข้อผิดพลาดดังกล่าวอาจสูงมาก เนื่องจากเงินจำนวนมากมักถูกเก็บไว้ในสัญญาอัจฉริยะ
เครื่องเสมือนสัญลักษณ์ของฉันเขียนด้วย PHP และ Python และใช้ Z3Prover จาก Microsoft Research เพื่อแก้สูตร SMT ที่เป็นผลลัพธ์
หัวใจหลักของมันคือการค้นหาหลายธุรกรรมที่ทรงพลังซึ่ง
ช่วยให้คุณค้นหาวิธีแก้ไขหรือช่องโหว่ แม้ว่าจะต้องใช้ธุรกรรมจำนวนมากก็ตาม
แม้ ซึ่งเป็นหนึ่งในเฟรมเวิร์กสัญลักษณ์ที่ทรงพลังที่สุดในการค้นหาช่องโหว่ของ Ethereum เพิ่งเพิ่มความสามารถนี้เมื่อไม่กี่เดือนที่ผ่านมา
แต่เป็นที่น่าสังเกตว่าสัญญาอีเธอร์นั้นซับซ้อนกว่าและทัวริงก็เสร็จสมบูรณ์
PHP แปลซอร์สโค้ดของสัญญาอัจฉริยะ RIDE เป็นสคริปต์ python ซึ่งโปรแกรมจะแสดงเป็นระบบที่เข้ากันได้กับ Z3 SMT ของสถานะสัญญาและเงื่อนไขสำหรับการเปลี่ยน:
ตอนนี้ฉันจะอธิบายสิ่งที่เกิดขึ้นภายในโดยละเอียดยิ่งขึ้น
แต่ก่อนอื่น ขออธิบายสักสองสามคำเกี่ยวกับภาษาสัญญาอัจฉริยะของ RIDE
เป็นภาษาการเขียนโปรแกรมเชิงฟังก์ชันและนิพจน์ที่ขี้เกียจโดยการออกแบบ
RIDE ทำงานแยกกันภายในบล็อกเชนและสามารถดึงและเขียนข้อมูลจากที่เก็บข้อมูลที่เชื่อมโยงกับกระเป๋าเงินของผู้ใช้
คุณสามารถแนบสัญญา RIDE กับกระเป๋าเงินแต่ละใบได้ และผลของการดำเนินการจะเป็นจริงหรือเท็จเท่านั้น
TRUE หมายความว่าสัญญาอัจฉริยะอนุญาตให้ทำธุรกรรมได้ และ FALSE หมายความว่าห้ามการทำธุรกรรม
ตัวอย่างง่ายๆ: สคริปต์สามารถห้ามการโอนได้หากยอดคงเหลือในกระเป๋าสตางค์น้อยกว่า 100
ตัวอย่างเช่น ฉันจะใช้ Wolf, Goat และ Cabbage แบบเดียวกัน แต่นำเสนอแล้วในรูปแบบของสัญญาอัจฉริยะ
ผู้ใช้จะไม่สามารถถอนเงินจากกระเป๋าเงินที่มีการปรับใช้สัญญาได้จนกว่าเขาจะส่งทุกคนไปยังอีกด้านหนึ่ง
#Извлекаем положение всех объектов из блокчейна
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 จะแปลงเป็นคำอธิบายระบบที่เข้ากันได้กับ Z3Prover SMT ใน Python
ข้อมูลถูกรวมไว้ในลูป โดยที่ตัวแปรหน่วยเก็บข้อมูลจะได้รับดัชนี 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] )
เงื่อนไขจะถูกจัดเรียงและแทรกลงในเทมเพลตสคริปต์ที่ออกแบบมาเพื่ออธิบายระบบ SMT ใน Python
แม่แบบว่างเปล่า
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 เพื่อให้เข้าถึงได้ฟรี
ที่มา: will.com