Bí mật về mã nguồn không thể bị hack

Mùa hè năm 2015, một nhóm tin tặc thiện chiến nhất thế giới được Bộ Quốc phòng Hoa Kỳ thuê bẻ khóa phần mềm đặc biệt nhưng đành phải bó tay sau nhiều tháng vật lộn.

Các thiết bị bay ( drone) sẽ được ưu tiên cài đặt phần mềm chống hack.

Mục tiêu cụ thể của nhóm tin tặc “Red Team” là chiếc trực thăng quân sự không người lái “ Little Bird” nằm tại cơ sở sản xuất của Boeing ở Arizona. Tất cả những gì mà nhóm tin tặc này cần làm là hack vào hệ thống máy tính kiểm soát bay trên chiếc trực thăng.

Phần mềm của Little Bird do chính Cơ quan đặc trách kế hoạch nghiên cứu quốc phòng cao cấp Hoa Kỳ (DARPA) viết. Với công nghệ hiện tại, không có phương tiện nào hack được hệ thống máy tính của chiếc trực thăng này. Mã nguồn của nó miễn nhiễm với mọi kỹ thuật xâm nhập hiện nay.

Ngay cả khi Red Team được gia hạn thêm vài tháng nữa với đầy đủ nguồn lực cần thiết nhưng cũng đành bó tay trước Little Bird.

Mã nguồn chống hack

Tháng 10/1973, Edsger Dijkstra có ý tưởng tạo ra loại mã nguồn hoàn hảo, hoàn toàn miễn nhiễm với các thể loại lỗi. Ông có ý tưởng viết các chương trình máy tính hoạt động chuẩn xác và chặt chẽ như định lý toán học.

Ý tưởng này được Edsger Dijkstra trình bày trong cuốn “Nguyên tắc Lập trình” viết năm 1976 cùng Tony Hoare. Cả Dijkstra và Hoare đều được trao giải thưởng Turing Award danh giá nhất trong lĩnh vực khoa học máy tính.

Edsger Wybe Dijkstra là nhà khoa học máy tính Hà Lan. Ông được nhận giải thưởng Turing cho các đóng góp có tính chất nền tảng trong lĩnh vực ngôn ngữ lập trình.

Tuy nhiên, tầm nhìn của cả hai đã không thực hiện được nhiều năm sau đó. Lý do rất đơn giản: rất khó gắn chức năng cho một chương trình bằng các quy tắc logic hình thức. Phải tới hơn 4 thập kỷ sau người ta mới tạo ra loại phần mềm có mã nguồn siêu an toàn.

Không như hầu hết mã nguồn máy tính hiện nay, vốn được viết và đánh giá chủ yếu trên môi trường làm việc cụ thể, loại phần mềm mới được viết theo dạng chứng minh toán học. Mỗi mệnh đề là sự tiếp nối của logic trước đó. Cả chương trình là một tổng thể hoàn hảo giống như định lý đã được nhà toán học chứng minh.

Dạng phần mềm này đang được nhiều công ty, tổ chức thực nghiệm, trong đó có quân đội Hoa Kỳ và những công ty công nghệ như Microsoft và Amazon.

Đây là nhu cầu thiết yếu trong bối cảnh các hoạt động kinh doanh và xã hội được giao dịch trực tiếp qua mạng. Trước đây, khi máy tính bị cách ly tại nhà và văn phòng, các lỗi lập trình chẳng có mấy tác động, cùng lắm chúng chỉ khiến phần mềm bị lỗi phải khởi động lại.

Nhưng thời nay, chỉ cần một lỗi nhỏ trong mã nguồn cũng đủ tạo ra những lỗ hổng bảo mật nghiêm trọng trên các thiết bị nối mạng. Sai sót đó có thể mở toang “cổng hậu” cho phép kẻ tấn công ung dung chiếm trọn hệ thống, đánh cắp toàn bộ dữ liệu và gây ra rất nhiều thiệt hại bổ sung khác.

Kathleen Fisher, nhà khoa học máy tính của trường đại họcTufts, trưởng nhóm dự án HACMS.

Dự án HACMS

HACMS là dự án trực thuộc DARPA có nhiệm vụ tạo ra loại thiết bị bay không thể hack được. Phần mềm chạy thiết bị là dạng nguyên khối (monolithic), có nghĩa nếu kẻ tấn công xâm nhập được vào một phần, những phần khác sẽ tự động mở toang ra.

Biết rõ nhược điểm này, nhóm HACMS đã dành ra hai năm để chia nhỏ mã nguồn chiếc máy tính kiểm soát nhiệm vụ của thiết bị bay.

HACMS cũng viết lại toàn bộ cấu trúc phần mềm, sử dụng “các khối xây dựng có độ đảm bảo cao”, một dạng công cụ cho phép chuyên gia lập trình kiểm tra độ tin cậy của mã nguồn.

Phương pháp này đã được chứng thực an toàn, kể cả khi ai đó xâm nhập được vào một phần cũng không thể tiếp cận các phần khác như vẫn làm trước đây. Các nhà lập trình HACMS sau đó đã cài đặt phần mềm này cho chiếc Little Bird.

Chiếc trực thăng Little Bird.

Cuộc sát hạch với Red Team cho thấy một phần của mã nguồn chiếc trực thăng đã bị xâm nhập nhưng nhóm tin tặc này không thể kiểm soát các chức năng thiết yếu khác.

Từ cuộc thực nghiệm trên Little Bird, DARPA đã áp dụng các công cụ và kỹ thuật của dự án HACMS cho nhiều lĩnh vực quân sự khác như vệ tinh, xe tự hành hộ tống.

Những nỗ lực khác

Bảo mật và tin cậy là hai mục tiêu chính mà phương pháp xây dựng phần mềm “không thể hack” hướng tới. Năm 2014, chỉ một lỗi nhỏ về mã nguồn cũng mở toang cánh cửa cho khủng hoảng bảo mật mang tên “Heartbleed”.

Heartbleed nghiêm trọng tới mức nó suýt làm sập toàn bộ hệ thống mạng Internet hiện nay. Rồi một năm sau, hai hacker mũ trắng đã xác nhận nỗi lo sợ lớn nhất mà con người sắp sửa đối mặt – đó là những chiếc xe hơi kết nối Internet có thể bị đột nhập và kiểm soát từ xa.

Và như vậy, thiệt hại không còn là dữ liệu mà là chính tính mạng con người.

Heartbleed suýt làm sập toàn bộ Internet.

Hiểu rõ những nguy cơ đó, đã có nhiều nỗ lực xây dựng các hệ thống phần mềm siêu an toàn. Điển hình trong số này là dự án cộng tác DeepSpec do Appel (hiện đang làm cho HACMS) dẫn đầu.

Mục tiêu của DeepSpec là xây dựng một hệ thống “end-to-end” được chứng thực đầy đủ giống như máy chủ web. Nếu thành công, dự án sẽ nhận được khoản tiền đầu tư 10 triệu USD từ Quỹ Khoa học Quốc Gia Hoa Kỳ.

Tại Microsoft Research, các kỹ sư phần mềm cũng đang bận rộn với hai dự án đầy tham vọng. Dự án “Everest” muốn tạo ra phiên bản xác thực của HTTPS, giao thức an toàn của trình duyệt web, vốn được xem là nguồn cơn gây ra phần lớn các ác mộng bảo mật hiện nay.

Mục tiêu của dự án thứ hai là xây dựng các thông số kỹ thuật xác thực cho các hệ thống vật lý-mạng như thiết bị bay không người lái, giống như mô hình thiết bị bay mà HACMS đã thử nghiệm ở trên.

Gia Nguyễn

Theo Zing