SMT solvers support stack-based incremental solving, but it only supports going back and forth at the end of the history chain and needs manual creation of checkpoints. I want an SMT solver with continuous learning that works out-of-the-box. If a solver previously checked conditions A and B independently, that information could be used later to make checking for A && B faster. I believe a solver with this optimization will significantly improve the performance of many research projects that rely on satisfiability checking.

To be more specific, symbolic execution engines will greatly benefit from this optimization. State-of-the-art symbolic execution engines are caching terms on the execution side to reduce the number of calls to SMT solvers. This optimization surely helps, but it is still pretty limited. Doing similar optimizations on the solver side is more promising to me since solvers have a better context to utilize that information. There is a report that nonoptimized stack-based incremental solving already gives 5x speedup, and I believe we can achieve greater speedup with an optimization based on continuous learning.

I am recently working on a CLI tool to manage and distribute CTF problems. While I was implementing the remove repository operation, I got an unexpected Access is denied. (os error 5) message on stable-x86_64-pc-windows-msvc toolchain (Rust 1.31.1).

fs::remove_dir_all(...) in this code was emitting the error.

let mut repo_index = env.data_dir().read_repo_index()?;

let image_list = runtime.block_on(docker::list_images(env))?;
if docker::image_from_repo_exists(&image_list, repo_name) {
    Err(SomaError::RepositoryInUseError)?;
}

let repository = repo_index
    .remove(repo_name)
    .ok_or(SomaError::RepositoryNotFoundError)?;
env.data_dir().write_repo_index(repo_index)?;

remove_dir_all(repository.local_path())?;

env.printer().write_line(&format!(
    "Successfully removed repository: '{}'.",
    &repo_name
));

Ok(())

I first ensured that no program is using files inside the directory. Then, I started searching about the issue. Surprisingly, it was a long-standing issue in the standard library from 2015 (#29497).

According to @pitdicker’s comment, problems with the current remove_dir_all implementation on Windows are:

  • cannot remove contents if the path becomes longer than MAX_PATH
  • files may not be deleted immediately, causing remove_dir to fail
  • unable to remove read-only files

Mine was the third case. .git/objects/pack contained files with read-only attributes, which caused the denial of the access. This behavior was surprising because I had no problem deleting the directory with File Explorer or on Linux. Apparently, this is the default behavior of Windows API, and Python had a similar issue. I agree to Tim Golden’s comment which says that “this, unfortunately, is the classic edge-case where intra-platform consistency and inter-platform consistency clash,” but I hope to have an easy fix in Rust like Python’s onerror argument instead of manually writing a directory recursion with permission handling.

The second problem is also noteworthy. The core reason for it is that unlike POSIX API, Windows file deletion API does not delete the file immediately but mark it for “delete later.” Therefore, even though DeleteFile call returns, it is not guaranteed that the file is actually deleted from the file system. Racing the File System talk in CppCon2015 mentions how to wrongly delete a directory tree on Windows. Unfortunately, this is the way how Rust’s remove_dir_all is implemented.

Slide from “Racing the File System”

As a result, the issue is causing spurious failures in rustup (#995). Also, tempdir and Maskerad implemented their version of remove_dir_all to bypass this problem. There was a PR (#31944) to fix this problem, but it was not merged to the upstream because of the difficulty of defining reasonable cross-platform behavior for Windows and Linux, the complexity of permission handling, and the inactivity from the original author.

The best solution, for now, seems using remove_dir_all crate which is based on PR #31944. I understand that it is hard to define the reasonable behavior for this kind of operations especially for cross-platform projects, but at least I could have saved much time if these edge cases were listed in the official documentation.

창의IT설계는 우리 학과의 간판 과목으로 한 학기 동안 자유 주제로 자신이 “창의IT스럽다”고 생각하는 프로젝트를 진행하는 과목이다. 총 네 단계로 이루어져 있으며 1, 2는 팀으로, 3, 4는 개인으로 진행하며 1, 2에서는 학기별로 주제를 변경하고 3, 4는 한 주제를 1년동안 진행하는 경우가 많다. 나는 자신이 원하는 프로젝트를 마음대로 진행할 수 있다는 자율성과, 학점을 통한 압박으로 마냥 놀지 못하게 하는 강제성이 절묘하게 시너지를 내는 훌륭한 과목이라고 생각한다. 창의IT융합공학과 진학을 선택하면서 고려했던 것도, 어차피 어느 학교에 가든 관심 있는 기술들을 바탕으로 개인 프로젝트를 진행할텐데 창의IT설계 과목 덕분에 주마다 프로젝트 진행 시간도 보장해주고 학점까지 챙겨갈 수 있으니 훨씬 집중하기 쉬운 환경이라고 생각했었다. 장학금 덕분에 신경 쓸 부분이 적어진다는 점도 마음에 들었었다.

사실 앞 문단은 은근슬쩍 끼워 넣은 학과 홍보였고, 본론으로 들어가면 학기 시작이 다가오면서 창의IT설계 3, 4 주제 선정 때문에 고민하고 있다. 교수님들께서는 방학 때 프로젝트를 시작하는 것을 추천하시지만 대부분의 학생들이 학기가 시작하고 프로젝트를 시작한다. 동아리에서 해킹을 하면서 기존 디버거들에 느꼈던 불만을 바탕으로 창의IT설계 3, 4에서는 바이너리 분석 및 디버깅 플랫폼을 주제로 하려고 생각하고 있었다. 시각적으로 좋은 프로젝트와 일상생활과 연관이 있는 프로젝트가 점수를 잘 받는 경향이 있기 때문에 학점 측면에서는 도박성이 있는 주제 선정이지만, 내가 즐겁게 할 수 있으면서 배우는 게 많고, 커리어에도 도움이 될 거라 생각해 이 주제를 일순위로 고려중이었다.

내가 해결하고 싶었던 문제들은 다음과 같다.

  • 디버깅 도구들의 높은 러닝 커브 낮추기
  • 바이너리 분석과 페이로드 제작 환경 통합
  • 중간 언어를 이용한 멀티 아키텍처 디컴파일링
  • codemap, qira, angr 등에 대한 쓰기 쉬운 프론트엔드 제공, 혹은 유사 기능 구현해 통합

주요 고려 대상이었던 건 gdbIDA 두 가지였다. gdb는 CUI에서 기반하는 명령어 암기 및 높은 러닝 커브가 문제라 생각했고, IDA는 높은 가격과 강력한 기능에 비해 아쉬운 UX(Undo 미지원 등)를 개선하고 싶었다. 또한 IDA처럼 실행 환경(주로 Unix)과 분석환경(주로 Windows)이 달라서 생기는 사소한 문제들도 해결할 수 있으면 좋겠다고 생각했다.

하지만 당연히 비슷한 생각을 하는 사람들이 있어서, Binary Ninja나, radare2 같은 2티어 바이너리 분석 툴들에서 이미 비슷한 문제에 대해 고민하고 있었다. 특히 radare2 같은 경우는 해외 커뮤니티에서 super stiff learning curve라는 이야기를 들을 정도로 어디서부터 시작하면 좋을지 모르게 생겼었는데, 최근에 웹 UI를 도입하면서 사용성이 크게 개선된 것처럼 보였다.

Radare2 Web UI

내가 생각하고 있던 구조도 서버에서 바이너리를 실행하고 웹 기반 GUI로 상호작용 하는 것이었는데, radare2의 웹 UI와 특징이 많이 겹쳤다. Binary Ninja는 웹UI는 아니지만 이것도 쓰기 좋은 크로스 플랫폼 UI를 제공하기 때문에 UI 사용성에서는 크게 우위를 보이기 힘들 것이라는 생각이 들었다.

중간 언어를 이용한 디컴파일링 기능은 Hex-Rays 만큼은 당연히 구현하지 못하겠지만, 함수 시그니처 인식, 조건문과 반복문 정도만 구현해도 무료 도구 치고는 경쟁력을 가질 수 있다고 생각했다. 하지만 radare2에서 이미 구현중이었고, Binary Ninja의 로드맵에도 주 목표 중 하나로 제시되어 있었다. 조사하다보니 lldb, gdb, vdb, windbg에 대한 추상화 레이어를 제공하는 Voltron 같은 프로젝트도 있었고, 알아볼수록 기존에 잘 만든 도구들이 많아서 이 주제를 그대로 고르는 것이 맞는지 계속 고민된다. 만약 그대로 이 주제를 선택한다면 완성도는 Binary Ninja Python Prototype 정도를 목표로 하려고 한다. 또한, 기존 도구들에 비해 어떤 차별성을 가질 수 있을지를 더 심도있게 고민해야 할 것으로 보인다.

만약의 경우를 대비해 생각해 두고 있는 다른 주제들도 몇 개 있다. 첫 번째는 1학년 때 MS 이매진컵 주제였던 복셀 기반 월드 에디터 + 비주얼 프로그래밍 언어를 이용한 교육용 프로그래밍 플랫폼 프로젝트다. SangJa라는 이름으로 나갔었는데, JS가 처음이기도 했고 협업에 익숙하지 않아 코드 관리가 조금 아쉬웠지만 주제 자체는 훌륭했다고 생각한다. 지금 생각하고 있는 주제 중 “창의IT”에 제일 적합하다고 생각되기는 한다. 팀 프로젝트라 내가 마음대로 주제를 쓸 수 있는게 아니라서 만약 이 주제를 고르게 된다면 이전에 같이 진행했던 사람들에게 연락해 내가 주제를 다시 써도 되는지 물어보아야 할 것 같다.

두 번째 주제는 안드로이드 매크로다. G매크로류의 매크로 프로그램들은 PC만 지원하는 경우가 많은데, 안드로이드까지 지원을 확장하고 비전 기반 기능들을 추가하려고 생각하고 있다(체력바를 읽는다든지 카드 희귀도를 알아내서 리세마라를 해 준다든지). 이 주제를 하게 되면 본의 아니게 또 OpenCV와 한 학기를 보내게 될 것이다. 이것도 적다보니 오토핫키 안드로이드 열화 카피가 되는 건 아닌지 걱정된다. sl4a 같은 프로젝트도 있고…

원래는 미리 고민해서 개발을 시작하려고 했는데, 연구참여도 하고 동아리도 하다 보니 짧은 방학이 훌쩍 지나가버렸다. 이번 학기에는 기초필수 과목이 끝난 덕분에 학기중 연참을 하면서 창의IT설계와 연구참여 투탑 체제로 프로그래밍 비중이 높은 학기를 보내려고 계획하고 있다.

이번 주말에는 PLUS에서 두 번째 CTF로 Internetwache라는 대회에 참가를 했다. CTF는 알고리즘 대회들과는 달리 24시간 이상 팀원들이랑 같이 달리는 대회라 페이스 조절이 정말 중요한듯. 모든 문제 클리어 24위로 마무리! 덧붙여서 저번에는 SharifCTF라는 대회를 했는데 9등을 했다. 역시 갓갓동아리.

이번 대회에서 228 비트짜리 RSA를 뚫는 문제가 나왔는데, 소인수분해를 끝내도 OpenSSL 사용법이 어려워서 그걸로 private key를 생성하는 방법을 배우는데 오래 걸렸다. 그래서 다음에는 삽질 안 하려고 툴을 만듦.

rsa_private

.git 폴더 노출된 사이트에서 플래그 빼오는 문제도 있었는데, git 구조도 겸사겸사 공부하면서 재밌게 풀었다. 이런 지식들 하나하나는 작을지 몰라도 배우면서 점점 지식이 늘어나는게 느껴져서 재밌다.

토요일에는 USACO 플래티넘을 쳤는데 문제가 생각보다 어려웠다. 1번을 두 시간에 걸쳐서 짰는데 한 번에 통과해서 기분이 좋았다. 남은 2, 3번을 한 시간 정도 고민하고 나서 정신력이 부족해서 리타이어 했다. 열심히 풀었으면 두 문제는 풀 수 있었을 것 같지만 그렇게까지 빡세게 할 필요는 없을거라 생각했다. 나중에 풀 문제 목록에 넣어놓았는데 이것도 언제 풀 지는 모른다 ㅋㅋ

USACO가 12월에 플래티넘 처음 생겼을 때는 난이도가 좀 쉬웠는데, 그걸 의식해서 그런지 1월부터 난이도가 확 올라갔다. 옛날 골드가 챌린징한 부분이 좀 적어서 아쉽긴 했지만, 지금 플래티넘은 내가 재밌게 풀기에는 좀 어렵더라. 고등학교 때 국대 떨어지고 대학에서는 ICPC 팀이 없어서 알고리즘 대회를 요새는 즐겜모드를 표방하며 아주 열심히 치지는 않고 그냥 나한테 부담 안 되고 재밌게 느껴지는 수준으로만 열심히 하는 중이다. 뭘 하든 간에 본인이 즐거운게 중요하지 않겠습니까.