메모리 해제 오류를 잘 고치는데 특화된 MemFix를 살펴보자.
📌 MemFix란?!
메모리 할당해제( memory deallocation ) 오류를 자동으로 고친다.
➡ memory-leak, double-free and use-after-free1) 이론적으로 patch된 code가 옳다는 것을 보장한다.
2) 에러를 고침으로써 새로운 에러가 더 발생하지 않는다는 것을 보장하여
때문에 개발자가 더 이상 볼필요가 없다.🌱 Key Ideas
– 정적분석(Static Analysis) + Exact Cover Problem을 통하여, 메모리 해제 오류를 고친다.
memfix는 리눅스 커널 메모리 해제오류를 다음과 같이 최적의 방법으로 해결했다.
'Free-statement'의 집합을 찾고, 조합의 문제로 바꾸어서 해결한다.
🌳 Exact Cover Problem
NP-Complete 문제이다.
{A, B, C, D, E}의 집합 중 1,2,3,4,5가 한번씩만 체크되도록 하는 부분 집합을 찾아보자.
a, b를 선택하면 3은 없으므로 답이 아니다.
a, b, c를 선택하면 2가 두번 포함되므로 답이 아니다.
a, b, d를 선택하면 모두 한번씩 체크된다 -> {a,b,d} = solution
c, e를 선택하면 모두 한번씩 체크된다. -> {c, e} = solution
memfix는 memory 해제 오류를 가진 코드에서, free()문을 어디에 넣을지에 대한 문제를 exact cover problem으로 바꾸어서 해결한다.
(1) object Trace를 만들어서, 중요한 경로의 일들을 적는다.
q (o1) 입장에서 if문에서 true인 경우와 false인 경우에 대해 각각 object trace를 만든다.
p (o2) 입장에서의 object trace도 생성한다.
(2) 각각의 사이에 free문(candidate patch)을 넣어본다.
(3) 말이 되지 않는 patch를 제거한다.
두번째 trace에서, free(p) 문은 use after free이기 때문에 삭제된다.
세번쨰 trace에서도 free(q)는 use after free로 삭제된다.
(4) 삭제한 patch가 다른 trace에 있다면, 그 부분도 삭제한다.
(5) 다음과 같이 exact cover problem으로 치환한다.
(6) (3,p) (8,q)가 정답이 된다. 즉, 이를 통해 각 trace가 모두 '한번씩'만 해제가 되도록 한다.
(7) 따라서 patch를 적용하면 다음과 같다.
결론 = 정적분석 + exact cover problem
(1) 각 객체가 할당될 수 있는 trace를 모두 path별로 enumerate한다. -> 정적분석기의 역할
(2) 각각의 trace가 해제될 수있는 candidate를 넣는다.
(3) use-after-free가 나타날 수 있는 candidate를 삭제한다.
(4) 남은 것으로 exact cover problem문제를 해결한다.
(5) 그 patch를 적용한다.
🌳 APR 기술의 평가기준
1) Scalability : 큰 코드에 대해서도 오류를 고칠 수 있는가
2) Repairability : 얼마나 많은 오류를 고칠 수 있는가
3) Safety : 오류를 고치는 과정에서 새로운 오류를 만들어내지 않는가
4) Correctness : original error을 고쳤는가
Memfix는 safety와 corectness는 보장해주지만 scalability를 보장해주지는 않으며, repairability도 한계가 있다.
🔔 SAVER
Safety는 보장하면서, correctness를 조금 희생하고 scalability와 repairability를 매우 높인 기술이다.
