Xác minh chính thức về kiến ​​trúc mã hóa được sắp xếp theo thứ tự

Một bài báo kỹ thuật có tiêu đề “Xác minh bảo mật của kiến ​​trúc có độ tin cậy thấp” đã được xuất bản bởi các nhà nghiên cứu tại Đại học Princeton, Đại học Michigan và Cao đẳng Lafayette.

Tóm tắt:

“Từ quan điểm của phần mềm, các kiến ​​trúc có độ tin cậy thấp hoạt động trên dữ liệu luôn được mã hóa và giảm đáng kể mức độ tin cậy của phần cứng đối với một thành phần nhỏ không có phần mềm. Trong bài viết này, chúng tôi thực hiện xác minh chính thức hoàn chỉnh về kiến ​​trúc có độ tin cậy thấp cụ thể, kiến ​​trúc Mã hóa tuần tự (SE), để cho thấy rằng thiết kế này an toàn trước việc tiết lộ dữ liệu trực tiếp và các kênh bên kỹ thuật số cho tất cả các chương trình có thể. Trước tiên, chúng tôi xác định các yêu cầu bảo mật của ISA của kiến ​​trúc có độ tin cậy thấp SE. Nhìn lên trên, ISA này đóng vai trò như một bản tóm tắt của phần cứng cho phần mềm và được sử dụng để chỉ ra cách bất kỳ chương trình nào bao gồm các hướng dẫn này không thể rò rỉ thông tin, kể cả thông qua các kênh kỹ thuật số. Nhìn xuống dưới, ISA này là một đặc điểm kỹ thuật cho phần cứng và được sử dụng để xác định các nghĩa vụ chứng minh cho mọi triển khai RTL phát sinh từ các yêu cầu bảo mật cấp ISA. Chúng bao gồm cả rò rỉ kênh bên chức năng và kỹ thuật số. Tiếp theo, chúng tôi chỉ ra cách có thể thực hiện thành công các nghĩa vụ chứng minh này bằng cách sử dụng các công cụ xác minh chính thức thương mại. Chúng tôi chứng minh tính hiệu quả của kỹ thuật xác minh bảo mật RTL của mình đối với bảy cách triển khai chính xác và có lỗi khác nhau của kiến ​​trúc SE.”

Tìm giấy kỹ thuật tại đây. Được xuất bản vào tháng 2023 năm XNUMX (bản in trước).

Tan, Qinhan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik và Todd Austin. “Xác minh bảo mật của các kiến ​​trúc có độ tin cậy thấp.” bản in trước arXiv arXiv:2309.00181 (2023).

Đọc liên quan
Xác minh và kiểm tra an toàn và bảo mật
Xác minh chức năng đang được mở rộng vượt quá khả năng của nó để đảm bảo hệ thống an toàn và bảo mật. Hỗ trợ mới đến từ phần cứng và phần mềm.
Các khái niệm mới cần thiết để xác minh bảo mật
Tại sao việc đảm bảo rằng phần cứng hoạt động chính xác và có khả năng phát hiện các lỗ hổng có thể xuất hiện tại hiện trường lại khó đến vậy.

• Phân phối nội dung và PR được hỗ trợ bởi SEO. Được khuếch đại ngay hôm nay.
• PlatoData.Network Vertical Generative Ai. Trao quyền cho chính mình. Truy cập Tại đây.
• PlatoAiStream. Thông minh Web3. Kiến thức khuếch đại. Truy cập Tại đây.
• Trung tâmESG. Ô tô / Xe điện, Than đá, công nghệ sạch, Năng lượng, Môi trường Hệ mặt trời, Quản lý chất thải. Truy cập Tại đây.
• PlatoSức khỏe. Tình báo thử nghiệm lâm sàng và công nghệ sinh học. Truy cập Tại đây.
• ChartPrime. Nâng cao trò chơi giao dịch của bạn với ChartPrime. Truy cập Tại đây.
• BlockOffsets. Hiện đại hóa quyền sở hữu bù đắp môi trường. Truy cập Tại đây.
• nguồn: https://semiengineering.com/formal-verification-of-a-sequestered-encryption-architecture/