Baseband software is an important component in cellular communication. Unfortunately, it is almost impossible to implement baseband software correctly due to the complexity and the large volume of cellular specifications. As a result, dynamic testing has been widely used to discover implementation bugs in them. However, this approach suffers from the reachability problem, resulting in many missed bugs. Recently, a static approach was proposed for analyzing baseband software. However, this requires heavy manual analysis and is limited to message decoding, failing to support integrity protection, the most critical step in mobile communication. In this paper, we propose a novel, semi-automated approach, for analyzing integrity protection. To tame the complexity of baseband firmware, our approach utilizes probabilistic inference to identify the integrity protection function. In particular, our approach builds a factor graph from the firmware based on specifications and discovers the most probable function for integrity protection. Then, with additional manual analysis, our approach performs symbolic analysis to validate that its behavior conforms to the specification and reports any discrepancies. This can significantly reduce manual efforts for analysis, the primary limitation of the previous static analysis approach for baseband.
베이스밴드 소프트웨어는 셀룰러 통신에서 중요한 부분이다. 하지만 셀룰러 사양의 복잡성과 방대한 양으로 인해 베이스밴드 소프트웨어를 정확하게 구현하는 것은 거의 불가능하다. 이에 구현상 버그를 찾기 위해서 동적 테스트 방식이 널리 사용되어 왔지만, 해당 방식은 접근성 문제로 인해 탐지하지 못하게 되는 버그가 생기는 문제점이 존재한다. 최근 한 연구가 베이스밴드 소프트웨어 분석을 위한 정적 분석 방식을 제안했으나, 많은 수작업을 필요로 하고, 메시지 디코딩에만 적용이 가능하여 모바일 통신에서 가장 중요한 무결성 보호를 분석할 수 없다는 한계가 있다. 본 연구는 베이스밴드 소프트웨어의 무결성 보호를 분석하기 위한 새로운 반자동 분석 방식을 제안한다. 베이스밴드 소프트웨어의 복잡성을 완화하기 위해 해당 방식은 확률적 추론을 활용하여 무결성 보호 기능을 하는 함수를 찾아낸다. 이후 추가적인 수동 분석과 함께 심볼릭 분석을 하여 동작이 사양에 부합하는지 검증하고 일치하지 않는 부분을 보고한다. 이를 통해 베이스밴드에 대한 기존 정적 분석 방식의 가장 큰 한계였던 수작업을 크게 줄일 수 있다.
