Oops! It appears that you have disabled your Javascript. In order for you to see this page as it is meant to appear, we ask that you please re-enable your Javascript!

คอนเฟิร์ม! นักวิจัยกำลังจะสร้างโค้ดที่ป้องกันการแฮกได้แล้ว

อุปกรณ์หลากหลายประเภทต่างกำลังได้รับการเชื่อมต่อกับอินเทอร์เน็ตเพื่อใช้ประโยชน์ แต่นอกเหนือจากประโยชน์ที่ได้นั้น มันยังเพิ่มความน่ากังวลเกี่ยวกับอุปกรณ์เหล่านี้ซึ่งอาจกลายเป้าของแฮกเกอร์  โครงการระบบไซเบอร์ทางการทหารที่มีความน่าเชื่อถือสูง (High-Assurance Cyber Military Systems: HACMS) ซึ่งนำโดยหน่วยงานโครงการค้นคว้าวิจัยการป้องกันขั้นสูง (Defense Advanced Research Projects Agency: DARPA) มีเป้าหมายเพื่อพัฒนาเทคโนโลยีการตรวจพิสูจน์อย่างเป็นทางการ (Formal Verification) โดยซอฟต์แวร์นั้นถูกออกแบบให้สอดคล้องไปกับคุณสมบัติอย่างเป็นทางการ (Formal Specification) ที่จะทำให้มันสามารถป้องกันการแฮกได้

ความสำเร็จด้านเทคโนโลยีและอินเทอร์เน็ตได้กลายเป็นช่องทางที่ทำให้เกิดความช่ำชองในการละเมิดความปลอดภัย สำหรับแฮกเกอร์ที่ชำนาญแล้วการเข้าไปในระบบที่สลับซับซ้อนก็เหมือนกับการเล่นของเด็ก  ข้อผิดพลาดเพียงจุดเดียวก็สามารถทำให้ซอฟต์แวร์โค้ดของคุณโดนแฮกได้

ดังนั้น ประเด็นที่น่ากังวลสำหรับนักวิจัยด้านความมั่นคงปลอดภัยคือกระบวนการที่ถูกใช้สำหรับเขียนซอฟต์แวร์โค้ด โดยทั่วไปโปรแกรมจะถูกเขียนด้วยวิธีการที่ไม่เป็นทางการและทำการทดสอบเพื่อให้มั่นใจว่าโค้ดนั้นสามารถทำงานและให้ผลลัพธ์ตามที่ต้องการ

ในปีที่ผ่านมา เฮลิคอปเตอร์ทางการทหารชื่อว่า “Little Bird” แบบไม่มีคนขับได้ถูกทดสอบโดยทีมแฮกเกอร์ “Red Team”  ซึ่งภารกิจคือการเข้าควบคุมเฮลิคอปเตอร์ดังกล่าว ทีมทดสอบได้สิทธิ์เข้าถึงส่วนหนึ่งของระบบ “Little Bird” และสิทธิ์ดังกล่าวก็ไม่ได้เป็นประโยชน์สำหรับพวกเขาในการเจาะเข้าไปในระบบส่วนอื่น ทว่าเจตนาที่แท้จริงไม่ใช่เป็นการทดสอบซอฟต์แวร์ที่ใช้งานอยู่กับเฮลิคอปเตอร์

เพราะภารกิจนี้เป็นส่วนหนึ่งของระบบไซเบอร์ทางการทหารที่มีความน่าเชื่อถือสูง HACMS (High-Assurance Cyber Military Systems) ซึ่งเป็นโครงการที่ได้รับเงินสนับสนุนจากหน่วยงานโครงการค้นคว้าวิจัยการป้องกันขั้นสูง (DARPA)  โดยที่หน่วยงานนี้ได้พัฒนาระบบความปลอดภัยแบบใหม่ขึ้นสำหรับ “Little Bird”  และพบว่าตลอด 6 สัปดาห์ ทีมแฮกเกอร์ล้มเหลวในการเจาะระบบความปลอดภัยของ “Little Bird” แม้ว่าพวกเขาจะมีการเข้าถึงที่มากกว่าผู้โจมตีที่แท้จริง

แคธลีน ฟิชเชอร์ (Kathleen Fisher) กล่าวว่า “พวกเขาไม่สามารถที่จะเจาะระบบและขัดขวางการปฏิบัติการในทุกวิถีทาง” เธอยังกล่าวต่ออีกว่า “ผลลัพธ์นั้นทำให้หน่วยงานโครงการค้นคว้าวิจัยการป้องกันขั้นสูงต้องลุกยืนขึ้นและพูดว่า นี่คือสิ่งที่ดีงาม เราสามารถใช้เทคโนโลยีนี้ได้จริงแล้วในระบบที่สำคัญ”  ฟิชเชอร์ เป็นผู้จัดการซึ่งริเริ่มโปรแกรมของโครงการ HACMS และยังเป็นอาจารย์ผู้สอนด้านวิทยาศาสตร์คอมพิวเตอร์ที่มหาวิทยาลัยทัฟส์

“ระบบใหม่นี้อยู่บนพื้นฐานการตรวจสอบอย่างเป็นทางการ (Formal Verification)” ประโยคฮิตซึ่งกำลังได้ความนิยมในกลุ่มสังคมผู้สนใจความมั่นคงปลอดภัย การตรวจสอบอย่างเป็นทางการ (Formal Verification) คือเทคนิคการทดสอบซอฟต์แวร์โค้ด เหมือนกับการพิสูจน์ทางคณิตศาสตร์ แต่ละประโยคของการพิสูจน์เป็นผลมาจากประโยคก่อนหน้าด้วยตรรกะอย่างเป็นเหตุผล ซึ่งนี่เป็นวิธีการเดียวกันกับที่นักคณิตศาสตร์ใช้ในการพิสูจน์ทฤษฎี

ไบรอัน พาร์โน (Bryan Parno)  นักวิจัยด้านความปลอดภัยและการตรวจสอบอย่างเป็นทางการ หน่วยงานวิจัยของไมโครซอฟต์ กล่าวว่า “คุณกำลังเขียนสูตรทางคณิตศาสตร์ซึ่งอธิบายพฤติกรรมของโปรแกรมและใช้การตรวจสอบพิสูจน์บางอย่างเพื่อใช้ในการตรวจสอบความถูกต้องของประโยคนั้น”

กระบวนการนี้เกี่ยวข้องกับการตรวจความถูกต้องของข้อเท็จจริงระหว่างกัน (Cross checking) ที่ว่าโค้ดโปรแกรมต้องเป็นไปตามคุณสมบัติอย่างเป็นทางการที่กำหนดไว้ ซึ่งโดยพื้นฐานแล้ว คุณสมบัติอย่างเป็นทางการจะเป็นตัวกำหนดว่าโปรแกรมต้องทำอะไร

“เพื่อที่จะดูว่ามันทำงานอย่างไร ลองจินตนาการถึงการเขียนโปรแกรมคอมพิวเตอร์สำหรับรถหุ่นยนต์ซึ่งจะขับรถพาคุณไปร้านขายของชำ ในระดับการปฏิบัติการ คุณจะต้องกำหนดการเคลื่อนที่ของรถยนต์ให้มีการจัดลำดับไปถึงจุดหมายได้ – มันสามารถที่จะเลี้ยวซ้ายหรือขวา เบรกหรือเร่งความเร็ว เปิดหรือปิดเมื่อจบทริปการเดินทาง โปรแกรมของคุณจะต้องรวบรวมการปฏิบัติพื้นฐานทั้งหลายที่จัดเรียงลำดับอย่างเหมาะสม เพื่อที่ว่าในตอนจบคุณจะถึงร้านขายของชำไม่ใช่ถึงที่สนามบิน”

ซอฟต์แวร์ที่ติดตั้งใน “Little Bird” โดย HACMS จะถูกแบ่งออกเป็นส่วน ระบบนี้ถูกออกแบบมาเพื่อในกรณีที่แฮกเกอร์สามารถจัดการเข้าถึงส่วนใดส่วนหนึ่งแล้ว เขาจะไม่สามารถเข้าถึงส่วนอื่นได้ เช่นที่เกิดขึ้นในกรณีของ “Read Team” ซึ่งได้สิทธิ์ในระบบกล้องของ Little Bird แต่ก็ล้มเหลวที่จะแฮกเฮลิคอปเตอร์นั้นได้

หน่วยงานโครงการค้นคว้าวิจัยการป้องกันขั้นสูง (DARPA)  มีแผนที่จะใช้การตรวจสอบอย่างเป็นทางการ (Formal Verification) ในเทคโนโลยีทางการทหารที่หลากหลาย เช่น รถบรรทุกที่ขับเคลื่อนเองได้ และดาวเทียมสื่อสาร นี่ไม่ใช่แค่การป้องกันองค์กรเช่นที่หน่วยงานโครงการค้นคว้าวิจัยการป้องกันขั้นสูง (DARPA)  กำลังดำเนินการเรื่องเทคโนโลยีการตรวจสอบอย่างเป็นทางการ  บริษัทด้านเทคโนโลยีเช่น ไมโครซอฟต์ อเมซอน ก็กำลังลงทุนเพื่อพัฒนาผลิตภัณฑ์ลักษณะนี้ขึ้นมาเช่นกัน

ฝ่ายวิจัยไมโครซอฟต์ เรดมอนด์ กำลังดำเนินโครงการเอเวอร์เรสต์ (Everest) ซึ่งเป็นโครงการที่ตั้งใจให้การตรวจสอบอย่างเป็นทาง (Formal Verification) สำหรับการเชื่อมต่อที่ปลอดภัยประสบความสำเร็จโดยการสร้าง HTTPS เวอร์ชั่นผ่านการตรวจสอบ    อีกโครงการที่กำลังดำเนินการคือการสร้างคุณสมบัติอย่างเป็นทางการ (Formal Specification) สำหรับระบบไซเบอร์ทางกายภาพที่สลับสับซ้อน เช่น โดรน

การตรวจสอบอย่างเป็นทางการ (Formal Verification) สามารถนำมาใช้ในการสร้างซอฟต์แวร์ที่ป้องกันการแฮกสำหรับเทคโนโลยีสมัยใหม่ เช่น รถยนต์ที่ขับเคลื่อนด้วยตัวเองซึ่งเชื่อมต่ออินเทอร์เน็ต แฮกเกอร์สามารถเข้าควบคุมยานยนต์เหล่านี้ได้ง่ายและสามารถทำให้มันเคลื่อนที่ได้ตามที่ต้องการ  เช่นกันสำหรับอุปกรณ์ IoT (Internet of Things) ที่ได้เพิ่มขึ้นและมีนัยสำคัญเมื่อไม่กี่ปีที่ผ่านมา บ้านของพวกเรากำลังกลาย เป็นสมาร์ทโฮม ซึ่งนี่จะเป็นมากกว่าแค่อุปกรณ์ที่เชื่อมต่ออินเทอร์เน็ตและแฮกเกอร์จะไม่ลังเลที่จะแฮกเพื่อควบคุมมัน

 

แหล่งที่มา

https://fossbytes.com/confirmed-researchers-are-close-to-making-a-hack-proof-code/