Nhóm nghiên cứu do GS. Zhong Shao, chuyên ngành khoa học máy tính dẫn đầu, đã phát triển một hệ điều hành kết hợp kiểm tra thiết kế (cụ thể là kiểm tra tính ngang bằng của hai thiết kế về mặt logic) để bảo đảm một chương trình hoạt động đúng như mục đích của nhà thiết kế. Đây là một biện pháp bảo vệ ngăn chặn sự tấn công của mọi thiết bị từ các thiết bị gia dụng và thiết bị Internet kết nối vạn vật (IOT) cho đến ô tô tự lái và tiền tệ điện tử.

Từ lâu, các nhà khoa học máy tính đã tin rằng hệ điều hành của máy tính cần có lõi nhỏ đáng tin cậy để đẩy mạnh truyền thông giữa phần mềm và phần cứng của hệ thống. Nhưng, các hệ điều hành phức tạp có liên kết trong mã yếu - một yếu tố gần như không thể phát hiện bằng nghiên cứu truyền thống - làm cho hệ thống dễ bị tin tặc tấn công.

Một trong những đột phá của hệ điều hành CertiKOS là nó hỗ trợ sự trùng hợp, nghĩa là hệ điều hành này có thể chạy đồng thời nhiều chuỗi (chuỗi các lệnh lập trình) trên đa lõi của đơn vị xử lý trung tâm (CPU). Điều này làm cho CertiKOS tách khỏi các hệ thống kiểm tra cũ và cho phép nó hoạt động trên các máy móc đa lõi hiện đại. Cấu trúc của CertiKOS cũng được thiết kế để bổ sung những chức năng mới và được sử dụng cho các miền ứng dụng khác nhau.

Sự trùng hợp cho phép thực hiện chồng chéo nhiều chuỗi chương trình, khiến nó không thể xem xét tất cả các tình huống và loại bỏ tất cả các rạn nứt trong hệ thống bằng phương thức kiểm tra truyền thống. Nhiều chuyên gia trong lĩnh vực này từ lâu tin rằng tính phức tạp của hệ thống cũng khiến cho việc kiểm tra tính chính xác của chức năng trở nên khó khăn hoặc quá tốn kém.

Trong quá trình xây dựng hệ thống CertiKOS, nhóm nghiên cứu đã kết hợp logic hình thức và các kỹ thuật mới kiểm tra suy diễn theo lớp. Các nhà khoa học đã thận trọng tách các thành phần phụ thuộc lẫn nhau của lõi, tổ chức mã thành bộ sưu tập lớn gồm các mô đun theo thứ bậc và ghi thông số toán học cho hành vi dự kiến của mỗi mô đun. Phương thức kiểm tra suy diễn hình thức được sử dụng để kiểm tra hệ thống khác với phương pháp thông thường kiểm tra độ tin cậy của một chương trình, trong đó, bộ ghi mã kiểm tra chương trình trong nhiều kịch bản.

GS. Shao cho rằng: "Một chương trình có thể được viết chính xác đến 99%, nhưng tin tặc vẫn có thể tấn công vào trong một thiết lập cụ thể làm cho chương trình không hoạt động như mong đợi. Chuyên gia viết phần mềm làm việc hướng tới những mục đích tốt đẹp, nhưng không thể lường trước mọi tình huống".

Andrew Appel, Giám đốc Tập đoàn DeepSpec thuộc Quỹ khoa học quốc gia và là Giáo sư chuyên ngành khoa học máy tính tại Trường Đại học Princeton coi hệ điều hành CertiKOS là "bước đột phá thực sự" và nhấn mạnh nó có thể được sử dụng làm cơ sở để xây dựng các hệ thống bảo mật cao. "Nhưng điều quan trọng là các phương pháp kiểm tra theo lớp mô đun được sử dụng trong CertiKOS, sẽ được áp dụng không chỉ cho các hệ điều hành, mà cả nhiều loại phần mềm", Appel nói.