지속성 메모리(Persistent memory)에서의 정보 흐름 보안

지속성 메모리(Persistent memory)는 런타임 효율성 향상과 전원 차단 및 시스템 충돌로부터 프로그램이 복구할 수 있는 능력을 포함하여, 시스템 전반에 걸친 많은 이점을 제공하는 최근 제안된 메모리 패러다임입니다. 최근 연구들이 관련 아키텍처에서 실행되는 프로그램의 기능적 정확성(functional correctness)을 증명하기 위한 기술들을 조사해 왔지만, 이와 직교하는 개념인 정보 흐름 보안(information flow security)에 대해서는 그렇지 않습니다. 본 논문에서는 단순한 어셈블리 언어를 모델링하는 비구조적 언어(즉, 루프(loops) 대신 goto를 사용하는 언어)를 위한 정보 흐름 논리(information flow logic)를 제공합니다. 우리는 메모리로의 잠재적인 비순차적 명령어 전파(out-of-order propagation)를 추론하기 위해 재정렬 간섭 자유(reordering interference freedom, rif)라는 개념을 사용하여 x86 어셈블리에 이 논리를 적용합니다. 그런 다음, 동일한 rif 개념이 지속성 메모리에서의 정보 흐름을 유사하게 추론하는 데 어떻게 사용될 수 있는지 보여줍니다.