격리된 암호화 아키텍처의 공식 검증

프린스턴 대학, 미시간 대학, 라파예트 대학 연구진이 "저신뢰 아키텍처의 보안 검증"이라는 기술 논문을 발표했습니다.

요약 :

“낮은 신뢰 아키텍처는 소프트웨어 관점에서 항상 암호화된 데이터에 대해 작동하며 소프트웨어가 없는 소규모 엔클레이브 구성 요소에 대한 하드웨어 신뢰 수준을 크게 줄입니다. 본 백서에서는 특정 저신뢰 아키텍처인 Sequestered Encryption(SE) 아키텍처에 대한 완전한 공식 검증을 수행하여 해당 설계가 가능한 모든 프로그램에 대한 직접적인 데이터 공개 및 디지털 사이드 채널로부터 안전하다는 것을 보여줍니다. 먼저 SE 낮은 신뢰 아키텍처의 ISA에 대한 보안 요구 사항을 정의합니다. 위쪽으로 보면 이 ISA는 소프트웨어용 하드웨어의 추상화 역할을 하며 이러한 명령어로 구성된 프로그램이 디지털 측면 채널을 포함하여 정보를 유출할 수 없는 방법을 보여주는 데 사용됩니다. 자세히 보면 이 ISA는 하드웨어 사양이며 ISA 수준 보안 요구 사항에서 발생하는 RTL 구현에 대한 증명 의무를 정의하는 데 사용됩니다. 이는 기능적 및 디지털 부채널 누출을 모두 다룹니다. 다음으로, 상업적 공식 검증 도구를 사용하여 이러한 증명 의무를 성공적으로 이행할 수 있는 방법을 보여줍니다. 우리는 SE 아키텍처의 7가지 서로 다른 정확하고 버그가 있는 구현에 대한 RTL 보안 검증 기술의 효율성을 입증합니다."

찾기 여기에 기술 문서가 있습니다. 2023년 XNUMX월 출판(사전 인쇄).

Tan, Qinhan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik 및 Todd Austin. “저신뢰 아키텍처의 보안 검증.” arXiv 사전 인쇄 arXiv:2309.00181 (2023).

관련 독서
안전 및 보안 검증 및 테스트
기능 검증은 안전하고 안전한 시스템을 보장하기 위해 기능 이상으로 확장되고 있습니다. 하드웨어와 소프트웨어에서 새로운 지원이 제공됩니다.
보안 검증에 필요한 새로운 개념
하드웨어가 올바르게 작동하고 현장에 나타날 수 있는 취약점을 감지할 수 있는지 확인하는 것이 왜 그렇게 어려운가요?

• SEO 기반 콘텐츠 및 PR 배포. 오늘 증폭하십시오.
• PlatoData.Network 수직 생성 Ai. 자신에게 권한을 부여하십시오. 여기에서 액세스하십시오.
• PlatoAiStream. 웹3 인텔리전스. 지식 증폭. 여기에서 액세스하십시오.
• 플라톤ESG. 자동차 / EV, 탄소, 클린테크, 에너지, 환경, 태양광, 폐기물 관리. 여기에서 액세스하십시오.
• PlatoHealth. 생명 공학 및 임상 시험 인텔리전스. 여기에서 액세스하십시오.
• 차트프라임. ChartPrime으로 트레이딩 게임을 향상시키십시오. 여기에서 액세스하십시오.
• BlockOffsets. 환경 오프셋 소유권 현대화. 여기에서 액세스하십시오.
• 출처: https://semiengineering.com/formal-verification-of-a-sequestered-encryption-architecture/