Vào mùa hè năm 2015, một nhóm tin tặc đã cố giành quyền điều khiển một chiếc máy bay trực thăng quân sự không người lái có tên “Little Bird”. Chiếc trực thăng có thiết kế tương tự với phiên bản có người lái thường xuyên được sử dụng trong các nhiệm vụ tác chiến đặc biệt của quân đội Mỹ, đóng tại một cơ sở của Boeing tại Arizona. Nhóm tin tặc có một khởi đầu thuận lợi: Tại thời điểm bắt đầu triển khai, chúng đã có thể truy cập vào một phần hệ thống máy tính của chiếc máy bay không người lái. Trên cơ sở đó, tất cả những gì chúng cần làm là đột nhập vào máy tính tích hợp bảng điều khiển bay của chiếc Little Bird và chiếc máy bay sẽ rơi vào tay chúng.
Khi dự án này khởi động, một nhóm các tin tặc được gọi là “đội Đỏ” được thuê để thực hiện việc xâm nhập. Ban đầu họ đã có thể cướp một chiếc máy bay lên thẳng một cách dễ dàng như thể chỉ là “câu trộm” Wi-Fi ở nhà bạn. Nhưng các kĩ sư đến từ Cơ quan các dự án phòng thủ tiên tiến trực thuộc Lầu Năm Góc (DARPA) đã triển khai một loại cơ chế bảo mật mới, một hệ thống phần mềm không thể bị trưng dụng. Những phần cốt yếu trong hệ thống máy tính của “Little Bird” sẽ không thể bị xâm nhập bằng những công nghệ sẵn có tại thời điểm đó, code của nó đáng tin cậy như một phép chứng minh toán học. “Đội Đỏ” sau đó mặc dù được cho thời gian là sáu tuần và thêm quyền truy cập đến mạng lưới máy tính của chiếc máy bay hơn rất nhiều đã thất bại trong việc bẻ khóa hàng phòng thủ của Little Bird.
Kathleen Fisher, giảng viên môn khoa học máy tính tại Đại học Tufts và quản lý của dự án High-Assurance Cyber Military Systems (HACMS) cho biết: “Họ đã không thể phá hoại và can thiệp vào quá trình vận hành bằng bất cứ cách nào. Kết quả này khiến cho tất cả mọi người tại DARPA phải bật dậy và thốt lên ngạc nhiên, chúng ta thực sự có thể đưa công nghệ này vào những hệ thống mà chúng ta cần phải bảo vệ.”
Công nghệ đẩy lùi các tin tặc là một kiểu lập trình phần mềm được biết đến dưới cái tên kiểm tra tính ngang bằng (formal verification). Khác với đa số code, được viết một cách không chuẩn thức và đáng giá chủ yếu dựa trên liệu nó có chạy được hay không thì những phần mềm được kiểm tra theo phương thức này rõ ràng như một chứng minh toán học: Mỗi một câu lệnh nối tiếp câu lệnh trước một cách logic. Toàn bộ chương trình đều có thể được kiểm thử một cách chắc chắn giống như cách các nhà toán học chứng minh các định lí.
Bryan Parno, nhà nghiên cứu về formal verification và an ninh tại Microsoft cho hay, “Bạn đang viết một công thức toán học mô tả hành vi của chương trình và sử dụng công cụ chứng minh để kiểm tra tính đúng đắn của câ lệnh đó” Mong muốn tạo ra phần mềm được kiểm tra tính ngang bằng đã có từ rất lâu gần như cùng lúc với khoa học máy tính. Trong suốt một thời gian dài, việc đó gần như là không thể với tới được một cách vô vọng. Nhưng những tiến bộ trong thập kỉ vừa qua trong các “phương pháp formal” đã đưa cách tiếp cận này đến gần hơn với những nghiên cứu chính thống. Ngày nay, phương thức này đang được nghiên cứu trong các trường đại học liên kết, quân đội Mỹ và các công ty về công nghệ như Microsoft và Amazon. Mối quan tâm ngày một lớn do sự gia tăng số lượng các giao dịch trực tuyến được sử dụng trong các hoạt động xã hội thiết yếu. Trước đây, khi mà máy tính bị cô lập và tách biệt giữa các hộ gia đình và văn phòng, bugs khi đó cũng chỉ là cái gì đó hơi bất tiện thì ngày nay chỉ cần một lỗi nhỏ khi code thôi đã mở ra vô vàn lỗ hổng bảo mật trên mạng lưới máy tính, cho phép bất cứ ai với hiểu biết về lĩnh vực này đươc mặc sức tự do tung hoảnh trong hệ thống máy tính.
Andrew Appel, giáo sư ngành công nghệ máy tính tại Đại học Princeton và chuyên gia đầu ngành trong lĩnh vực kiếm tra phần mềm nói rằng “ Vào thế kỉ 20, nếu một chương trình có một bug, nó có thể dừng hoạt động và chỉ có vậy. Thế nhưng vào thế kỉ 21 này thì chỉ một bug thôi đã có thể tạo ra một phương thức cho phép các tin tặc giành quyền kiểm soát chương trình và đánh cắp tất cả dữ liệu của bạn. Từ một bug dù có không tốt nhưng có thể tạm chấp nhận nó đã trở thành một lỗ hỏng tệ hơn rất nhiều.”
Giấc mơ về những chương trình hoàn hảo
Vào tháng 10 năm 1973, Edsger Dijkstra xuất hiện cùng với một ý tưởng cho việc tạo ra code không lỗi. Trong khi ở trong một khách sạn tại một buổi hội thảo, ông bất chợt nảy ra ý tưởng làm cho việc lập trình “toán học” hơn. Ông mô tả trong tự truyện của mình “Não tôi như có lửa đốt, tôi leo xuống giường lúc 2h30 sáng và viết liên tục trong hơn một tiếng đồng hồ” Đây chính là khởi điểm cho cuốn sách xuất bản năm 1976 của ông “A Discipline of Programming,” cùng với công trình của Tony Hoare, người cũng giống Dijkstra nhận được giải thưởng Turing, thiết lập một tầm nhìn mới cho việc kết hợp bằng chứng xác thực vào trong việc viết các chương trình.
Kathleen Fisher Đó không phải là một tầm nhìn mà khoa học máy tính có thể đi theo, phần lớn là do sau đó nhiều năm, người ta đã thấy nó thiếu thực tế hay nói thẳng thắn hơn là không thể được khi muốn cụ thể hóa một chức năng bằng cách dùng những nguyên tắc của logic hình thức.
Đặc tính kĩ thuật là một cách để xác định xem chính xác thì một chương trình máy tính làm gì. Và kiểm tra tính ngang bằng là mộ cách để chứng minh không còn chút nghi ngờ nào rằng code của một chương trình có đạt được đặc tính kĩ thuật đó không. Để hiểu nguyên lí của việc này, hãy tưởng tượng bạn viết một chương trình máy tính cho một chiếc ô tô robot để nó chở bạn tới một cửa hàng tạp hóa. Ở mức độ vận hành, bạn sẽ xác định những chuyển động của chiếc xe tại thời điểm vận hành để thực hiện một hành trình. Nó có thể rẽ trái hoặc phải, phanh hoặc tăng tốc, bật hoặc tắt ở cuối hành trình. Chương trình của bạn khi đó sẽ là một tập hợp của những quy trình cơ bản đó được sắp xếp hợp lí để sao cho cuối cùng thì bạn sẽ đến được cửa hàng tạp hóa chứ không phải tới sân bay.
Cách truyền thống và đơn giản để xem một chương trình có chạy được hay không là kiểm thử nó. Coders đưa vào những chương trình của họ một loạt cái yếu tố để đảm bảo (unit testing) chúng chạy đúng theo thiết kế. Nếu chương trình của bạn là một thuật toán điều khiển lộ trình một chiếc ô tô robot chẳng hạn, thì bạn sẽ phải test nó ở rất nhiều điểm. Phương pháp kiểm thử này giúp cho những sản phẩm phần mềm được làm ra vận hành trơn tru. Nhưng unit testing không thể đảm bảo phầm mềm sẽ luôn luôn chạy chính xác bởi không có cách nào để chạy một chương trình qua tất cả các inputs. Kể cả nếu thuật toán chạy thành công với tất cả mọi điểm đến mà bạn test, luôn luôn có khả năng nó sẽ ngừng hoạt động trong một vài trường hợp hiếm gặp và mở ra một kẽ hở an ninh. Trong những chương trình thật, những trục trặc có thể đơn giản như là lỗi tràn bộ đệm, khi mà một chương trình sao chép nhiều dữ liệu hơn mức và ghi đè lên một phần nhỏ bộ nhớ của máy tính. Đó là một lỗi tưởng chừng như vô hại nhưng lại khó có thể loại bỏ và có thể tạo điều kiện cho tin tặc tấn công hệ thống.
Các đặc tính kĩ thuật đòi hỏi phức tạp hơn là hành trình tới cửa hàng tạp hóa. Kĩ sư phần mềm có thể sẽ muốn viết một chương trình giúp công chứng và để lại dấu thời gian trên cái tài liệu theo thứ tự nhận được. Trong trường hợp này đặc tính kĩ thuật cần giải thích rằng bộ đếm luôn tăng để tài liệu nhận sau luôn có số lớn hơn tài liệu nhận trước và chương trình sẽ không bao giờ rò rỉ các key mà nó dùng để “kí tên” trên các tài liệu.
Việc này nói nghe thì quá đơn giản nhưng việc biến nó thành ngôn ngữ chuẩn để máy tính có thể áp dụng được thì khó hơn gấp bội.
Parno cho biết: “Tạo ra được một đặc tính kĩ thuật mà máy móc có thể đọc được nhìn chung là vô cùng khó khăn. Nói ‘không được để rò rỉ mật khẩu của tôi’ thì quá dễ nhưng biến nó thành một định nghĩa toán học chắc chắn sẽ đòi hỏi bạn phải suy nghĩ”
Một ví dụ khác, cho một chương trình sắp xếp một dãy số. Một kĩ sư đang cố gắng đặc tính hóa một chương trình sắp xếp có thể sẽ nghĩ ra những thứ như:
Với mỗi giá trị j trong danh sách, hãy đảm bảo điều kiện j ≤ j+1
Đặc tính kĩ thuật này đảm bảo rằng mọi giá trị trong danh sách đều nhỏ hơn hoặc bằng giá trị theo sau nó nhưng vẫn có một bug ở đây. Những kĩ sư lập trình đặt giả thiết là đầu ra sẽ là một hoán vị của đầu vào. Cụ thể là, nếu cho [7, 3, 5] họ kì vọng rằng chương trình sẽ trả về [3, 5, 7] và thỏa mãn định nghĩa. Nhưng [1, 2] cũng thỏa mãn bỏi Parno cho biết “nó là một danh sách sắp xếp chứ không phải là một danh sách sắp xếp mà chúng ta hi vọng nó là như vậy.”
Nói một cách khác, để truyền tải một ý tưởng mà bạn có về việc một chương trình nên làm gì vào một đặc tính kĩ thuật, loại bỏ mọi cách diễn giải có thể (nhưng không thỏa mãn) về chức năng của chương trình, là vô cùng nan giải. Và ví dụ ở trên đây là một ví dụ về một phần mềm sắp xếp hết sức đơn giản. Bây giờ hãy thử tưởng tượng nếu đó là một thứ gì đó trừu tượng hơn việc sắp xếp rất nhiều, ví dụ như việc bảo một mật khẩu. Ông nói thêm: “Nó có ý nghĩa gì về mặt toán học? Việc định nghĩa nó có thể sẽ cần phải viết một mô tả toán học về giữ bí mật có nghĩa là gì hay bảo mật một thuật toán được mã hóa là gì. Đây là những câu hỏi mà chúng tôi và rất nhiều người khác nữa đang tìm câu trả lời chính xác nhưng thật sự thì cơ hội rất mong manh”
Bảo mật dạng khối (Block-Based Security)
Khi viết những đặc tính kĩ thuật này cùng với những ghi chú đi kèm để cho chương trình chạy được, một chương trình bao gồm cả những thông tin kiếm tra tính ngang bằng có thể dài gấp năm lần một chương trình bình thường mặc dù cả hai đều trả về kết quả như nhau.
Trở ngại này có thể được loại bỏ phần nào bằng cách sử dụng các công cụ như các ngôn ngữ lập trình và các chương trình được thiết kế để trợ giúp các kĩ sư phần mềm tạo ra những đoạn code “chống bom”. Nhưng những năm 1970s những khái niệm này chưa tồn tại. Appel, trưởng nhóm nghiên cứu DeepSpec, một nhóm phát triển hệ thống máy tính được kiểm định cho hay “Có nhiều phần của khoa học và công nghệ chưa phát triển đủ để triển khai thành công ý tưởng đó thế nên khoảng những năm 1980 nhiều nhà nghiên cứu mất hứng thú và sự quan tâm tới vấn đề này.
Ngay cả khi những công cụ này được cải tiến, một trở ngại nữa lại xuất hiện: Không ai có thể chắc chắn rằng liệu nó có cần thiết hay không. Trong khi những người hào hứng với những phương pháp xác minh nói về những lỗi nhỏ nhặt trong code nhưng lại mô tả nó như những cái bugs nguy hiểm trầm trọng, thì mọi người nhìn ra xung quanh và thấy những chương trình máy tính vẫn chạy ổn. Đúng là thi thoảng chúng ngừng hoạt động đột ngột và khiến ta mấy một lượng công việc chưa được lưu và đôi khi sẽ phải khởi động lại nhưng nghe có vẻ cũng không phải cái gì quá ghê gớm lắm để chúng ta phải sử dụng những biện pháp kiểm định này. Vào thời điểm đó, ngay cả những nhà vô địch về kiểm định phần mềm cũng bắt đầu nghi ngờ về công dụng và tính hữu ích của nó. Vào những năm 1990, Hoare cha đẻ của “Hoare logic”, một trong những hệ thống lí luận về độ chính xác của một chương trình máy tính đầu tiên, đã thừa nhận rằng đây là một giải pháp đòi hỏi quá nhiều lao động chuyên sâu để giải quyết một vấn đề “không tồn tại”. Ông viết:
“Mười năm về trước, những nhà nghiên cứu phương pháp hình thức (và tôi là người đã sai lầm nhất trong số họ) đã dự đoán rằng việc lập trình sẽ bao hàm tất cả những tiện ích, trợ giúp mà việc kiểm định hứa hẹn sẽ mang lại….Nhưng thực tế thì thế giới không phải gánh chịu những ảnh hưởng nặng nề của những vấn đề mà nghiên cứu của chúng tôi muốn giải quyết khi khởi động nó.”
Sau đó mạng internet xuất hiện, những gì nó gây nên cho những lỗi mã hóa tương tự như những gì mà việc di chuyển bằng đường hàng không tác động lên sự lây lan của những căn bệnh truyền nhiễm. Khi mỗi máy tính đều được kết nối với nhau, những lỗi nho nhỏ nhưng có thể chấp nhận được lúc trước có thể dẫn đến hàng loạt những lỗi bảo mật.
Appel nói: “Đây là thứ mà chúng ta đã không thực sự hiểu hết. Đó là có một số loại phần mềm sẽ phải đối mặt với tất cả các tin tặc trên mạng. Thế nên chỉ cần có một bug trong phần mềm đó thôi, nó cũng có thể dễ dàng trở thành một lỗ hổng bảo mật.
Jeannette Wing
Khi mà các nhà nghiên cứu bắt đầu hiểu ra những mối nguy hại cho bảo mật của máy tính do mạng internet gây nên thì việc kiểm định các chương trình đã sẵn sàng để quay trở lại. Để bắt đầu, các nhà nghiên cứu đã có những bước tiến lớn trong công nghệ củng cố phương pháp hình thức: những cải tiến trong các chương trình hộ trợ như Coq và Isabelle; sự phát triển của những hệ thống logic mới (được gọi là những giả thuyết phụ thuộc vào chủng loại) cung cấp framework cho máy tính lí luận; và những bước phát triển trong “Ngữ nghĩa vận hành” – về bản chất, một ngôn ngữ có những từ ngữ phù hợp để thể hiện những gì mà một chương trình cần phải thực hiện.
Jeannette Wing, phó chủ tích Microsoft Research cho biết: “Nếu bạn bắt đầu bằng những đặc điểm viết bằng tiếng Anh, bạn vốn đã bắt đầu bằng một đặc điểm tối nghĩa. Bất kì một ngôn ngữ tự nhiên nào đều vốn rất mơ hồ. Trong kiểm định hình thức, bạn sẽ viết ra một đặc điểm chính xác, dựa trên toán học để lí giải những gì bạn muốn chương trình đó làm. “
Thêm vào đó, những nhà nghiên cứu các phương pháp hình thức cũng tiết chế những mục tiêu của họ. Vào những năm 1970 và đầu những năm 1980, họ đã mường tượng ra hệ thống máy tính kiểm định toàn diện, từ mạch điện cho tới phầm mềm. Ngày nay đa phần các nhà nghiên cứu phương pháp hình thức tập trung vào những phần nhỏ hơn của hệ thống nhưng có vai trò quan trọng và dễ bị tấn công hơn, ví dụ như hệ điều hành hay các giao thức mã hóa.
“Chứng tôi không tuyên bố là chúng tôi sẽ chứng minh toàn bộ hệ thống là chính xác, 100% đáng tin cậy cho tới từng bit, từng mạch điện. Nghe sẽ rất ngớ ngẩn nếu nói như vậy. Chúng tôi hiểu rõ hơn hết về những gì chúng tôi có thể và không thể làm được.”
Dực án HACMS minh chứng rằng, việc tạo ra những đảm bảo về độ bảo mật cho hệ thống máy tính bằng cách củng cố một phần nhỏ và cụ thể nào đó, là hoàn toàn có thể. Mục tiêu ban đầu của dự án là tạo ra một chiếc quadcopter (một loại máy bay trực thăng) không thể bị xâm nhập. Phần mềm có sẵn vận hành chiếc quadcopter là một loại nguyên khối, có nghĩa là nếu tin tặc đột nhập được vào một phần, hắn sẽ chiếm được toàn bộ. Vì thế nên, trong vòng hai năm, HACMS đã thiết lập việc chia mã code trên máy tính điều khiển nhiệm vụ của chiếc máy bay thành các phân vùng.
HACMS cũng viết lại kiến trúc của phần mềm sử dụng những gì Fisher, người quản lí sáng lập dự án, gọi là “những khối xây dựng có độ đảm bảo bảo cao” – những công cụ cho phép các lập trình viên chứng minh độ chân thực của code. Một trong những khối xây dựng đã qua kiểm định đó đi kèm với một minh chứng, đảm bảo rằng nếu một ai đó có thể truy cập vào một phân vùng, họ không thể tiếp tục xâm nhập tiếp sang những phân vùng khác.
Sau đó những lập trình viên của HACMS đã lắp đặt phần mềm được phân vùng nay lên chiếc Little Bird. Trong thử nghiệm chống lại nhóm tin tặc “Đội Đỏ”, họ cho những tin tặc này quyền truy cập vào một phân vùng điều khiển những bộ phận của trực thăng không người lái như máy ảnh nhưng không phải là một phần thiết yếu. Họ đảm bảo là về mặt toán học những tin tặc này sẽ không thể tìm được cách xâm nhập. “Họ chứng minh rằng về mặt máy móc thì những tin tặc này không thể phá vỡ và thoát ra khỏi phân vùng này. Nó chạy khá ổn định về mặt lí thuyết nhưng kiểm tra lại là cần thiết.”
Cùng năm đó, DARPA đã ứng dụng những công cụ và công nghệ từ dự án HACMS vào những lĩnh vực khác của công nghệ quân sự, có thể kể đến là các vệ tinh và xe tải hộ tống tự lái. Những sáng kiến sau đó đều nhất quán với cách mà kiểm định hình thức được phổ biến rộng khắp trong thập kỉ vừa qua. Mỗi dự án thành công lại khuyến khích cho những dự án tiếp theo.
Xác minh mạng Internet (Verifying the Internet)
Bảo mật và độ tin cậy là hai mục tiêu chính, tạo động lực cho các phương pháp hình thức. Và với mỗi ngày trôi qua, nhu cầu cải tiến cả hai tiêu chí này ngày một rõ ràng. Vào năm 2014, một lỗi nhỏ trong code, lẽ ra đã có thể bị tóm bằng phương pháp này, đã mở đường cho bug Heartbleed, đe dọa đánh sập mạng internet. Một năm sau một bộ đôi tin tặc đã khiến cho chúng ta trải qua nỗi khiếp sợ to lớn nhất, bằng những chiếc xe được kết nối internet, khi chúng giành được quyền kiểm soát một chiếc Jeep Cherokee.
Mối hiểm họa ngày một lên cao, các nhà nghiên cứu cũng tham vọng hơn. Để đáp lại tinh thần lạc quan của những nghiên cứu vào những năm 1970, dự án DeepSpec dẫn dắt bởi Appel (người cũng tham gia HACMS) cũng nỗ lực xây dựng một hệ thống tương tự như một chiếc máy chủ một trang web. Nếu thành công, nó sẽ giúp liên kết những thành công trước và sau trong suốt thập kỉ vừa qua. Tại Microsoft, các kĩ sư phần mềm cũng đang có hai dự án đầy tham vọng. Một là Everest dự án nghiên cứu phiên bản được kiểm định HTTPS, giao thức bảo vệ các trình duyệt web và Wing gọi nó là “Gót chân A-sin của mạng Internet”
Hai là dự án tạo ra những đặc điểm kĩ thuật được kiểm định cho những hệ thống công nghệ cao phức tạp như drone (trực thăng không người lái). Thách thức này có thể cân nhắc được. Trong khi những phần mềm điển hình tuân theo những bước đơn lẻ, rõ ràng, những chương trình điều khiển drones sử dụng cách học hỏi để đưa ra các quyết định dựa trên những dữ liệu từ môi trường. Mặc dù rất khó để có thể lí luận và đưa nó vào thực tiến nhưng trong suốt những năm vừa qua phương pháp hình thức đã có những tiến bộ rất đáng kể và Wing rất lạc quan về việc các nhà nghiên cứu những phương pháp này sẽ sớm tìm ra giải pháp.
Nguồn: https://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/
Techtalk via Viblo
