When operationally and managerially independent constituent systems are integrated to form a System of Systems (SoS), cybersecurity vulnerabilities can be exploited by cyber threats that can break the security requirements of SoS due to its collaborative nature. Using model-checking technique to gen- erate test cases automatically can potentially aid in discovering vulnerabilities. However, security test case generation is time-consuming, error-prone, and labor-intensive; therefore, it is desirable to fully or partially automate security testing processes. We propose the automatic test data generation using formal models presented as communicating sequential processes. We use the model-checking technique that generates counterexamples when the specified security properties are violated. Our approach then converted those counterexamples into executable test data by applying the conversion rule and defined mapping algorithm. We demonstrate our approach with an experiment using an operation of an air traffic control (ATC) system, a representative of SoS. We developed an agent simulation program to test the operation of the ATC by using the generated test data and evaluating it in terms of vulnerability identification. We incorporated four attack types, and our experimental results show that the security tests generated from the models can identify the known vulnerabilities in the ATC system.
운영상 및 관리상 독립적인 구성 시스템을 통합하여 시스템 오브 시스템(SoS)를 형성할 경우 협업적 특성으 로 인해 SoS의 보안 요구사항을 위반할 수 있는 사이버 위협에 의해 사이버 보안 취약점이 악용될 수 있다. 모델 체킹 기술을 사용하여 테스트 사례를 자동으로 생성하면 잠재적으로 취약성을 발견하는 데 도움이 될 수있다. 그러나보안테스트케이스생성은시간이많이걸리고오류가발생하기쉬우며많은수고가들기 때문에 보안 테스트 프로세스를 완전히 또는 부분적으로 자동화할 필요가 있다. 본 연구에서는 통신 순차 프로세스기반 모델을 사용한 자동 테스트 데이터 생성을 제안한다. 지정된 보안 속성을 위반할 때 반례를 생성하는 모델 체킹 기술을 사용하며, 그런 다음 우리의 접근 방식은 변환 규칙과 정의된 매핑 알고리즘을 적용하여 이러한 반례를 실행 가능한 테스트 데이터로 변환한다. 제안하는 기법을 대표적인 SoS인 항공 교통 관제(ATC) 시스템에 적용하는 실험을 수행하였다. ATC 대상 에이전트 시뮬레이션 프로그램을 개발하여, 생성된 테스트 데이터가 취약성 탐지 측면에서 어떠한지 평가하였다 네 가지 공격 유형을 포함하였으며, 실험 결과 모델에서 생성된 보안 테스트가 ATC 시스템의 알려진 취약성을 식별할 수 있음을 확인하였다.
