글쓴이 ·0개의 댓글

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.

글쓴이 ·0개의 댓글

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.

글쓴이 ·0개의 댓글

오랜만의 블로그 포스트가 알고리즘 대회 후기가 될 것이라고 예상하지 못했는데, 마지막 글이 올라온지도 꽤 됐고 이번 대회에서 하고 싶은 얘기도 있어서 포스팅을 하기로 했다. 현재 나는 작년 ICPC 이후로 공식적으로는 경쟁 프로그래밍을 은퇴한 상태다. 평소에 공부하고 시간 쓰는건 완전히 멈췄고, 대신 거기 쓰던 시간을 워게임 등 해킹 문제를 풀거나 졸업 후 진로 준비에 쓰고 있다. 이렇게 말하니까 알고리즘 공부에 계속 시간을 많이 쓰고 노력했던 것 같지만 은퇴 선언 이전에도 실질적으로 손을 놓은지는 꽤 됐다. 지금은 티셔츠나 상금 등 부상 주는 대회를 가끔 부담 없이 나가는 걸 목표로 하고 있다.

원래 이번 코드잼은 Rust로 알고리즘 라이브러리를 짜고 그걸 써서 대회를 치고, 대회와 대회 사이에 라이브러리를 보강한 뒤 대회 이후 프로젝트를 다듬어서 공개한다는 원대한 계획과 함께하고 있었다. 하지만 코드잼 플랫폼이 바뀌고 Rust가 지원 언어 목록에 없어서 라이브러리 작성에 대한 관심이 급격하게 식었고, 다익스트라 알고리즘 정도만 겨우 구현된 Rust 알고리즘 라이브러리는 지금까지 존재했던 나만 알고 있다가 비트의 저편으로 사라졌던 많은 개인 프로젝트와 마찬가지로 GitHub 개인 저장소에 조금 더 머무르다 영영 사라질 예정이다. Cargo 배포용으로 이름도 지어줬는데 불쌍한 친구…

올해 코드잼 연습 세션을 치고 나서 느꼈던 건 생각하는 능력 자체는 예상보다 덜 줄었고, 전통적인 테크닉을 떠올리거나 코드를 빠르게 짜는 능력은 예상보다 많이 줄었다는 거였다. 여기서 “생각하는 능력”은 연습 세션 3번 Steed 2 Cruise Control에서 여러 속도로 달리는 말들 사이의 불변조건을 구하는 능력을 말하고 “전통적인 테크닉”은 R1A 3번 Edgy Baking을 보고 냅색이니까 DP로 풀면 뚝딱 할 수 있겠다는 걸 떠올리는 능력을 말한다. 연습 세션부터 이번 R1A까지 예전에 비해 같은 코드를 짜는데 시간이 훨씬 오래 걸린다는게 느껴졌다.

이번 대회를 치면서 좀 놀랐던 점은 대회 중 오랜만에 초심을 되찾은 기분을 느꼈던 것이다. 내 풀이에서 놓친 점을 찾았을 때 예전 같았으면 쉬운 문제에서 실수했다고 자책했겠지만 이번 대회에서는 웬일로 풀이의 빠진 구멍을 채워 나가는 느낌이 즐겁게 느껴졌다. 알고리즘 대회에서 어려운 문제에 도전하는 지적 만족감을 느낀 적은 많았지만, 문제를 푸는 것이 아니라 시간 제한을 두고 대회를 치는 것을 즐겁다고 생각해 본지는 꽤 오래됐다. 평소에 연습을 많이 안 하니 예전만큼 잘하지 못하는 건 당연하다고 생각하면서도 무의식 속에서는 그래도 내가 경력이 얼마인데 못해도 어느 정도는 해야 한다는 부담을 느끼고 있었다고 생각한다. 나도 내가 무의식에서 어떤 생각을 하는지 완전히 모르지만, 공식적으로 은퇴했다고 선언했던게 그런 부담을 낮춰준 게 아닌가 추측하고 있다. 바뀐 플랫폼에서 스코어보드가 문제 페이지에 보이지 않는 것도 도움이 됐다.

원래 대회 후기는 문제 풀이도 함께 올리는게 전통이므로 간단한 풀이도 함께 첨부한다.

  • A: 전체 초콜릿 개수를 세고, \text{(number of H piece)}\times \text{(number of V piece)}로 나누어 떨어지는지 확인한다. 가로 분할선과 세로 분할선의 위치는 초콜릿 개수를 통해 독립적으로 판단 가능하며, 분할선들의 위치가 정해지면 분할된 각 칸에 초콜릿이 균등하게 들어가 있는지 확인한다.
  • B: 계산이 특정 시간 안에 끝날 수 있는지를 판단하는 판별 함수를 작성하고 파라메트릭 바이너리 서치를 수행한다. 판별 함수는 각 계산원이 그 시간까지 처리 가능한 비트의 수를 계산한 뒤 정렬해 큰 순서대로 R개를 뽑아 B 이상이면 처리 가능한 것이다.
  • C: 0-1 냅색. 2 \cdot w_i h_i를 미리 P에서 빼고, 물건의 크기가 min(w, h) 점수는 \sqrt{w^2 + h^2}인 냅색을 수행한다.

글쓴이 ·0개의 댓글

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

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

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

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

주요 고려 대상이었던 건 gdb와 IDA 두 가지였다. 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설계와 연구참여 투탑 체제로 프로그래밍 비중이 높은 학기를 보내려고 계획하고 있다.