Property Guided Secure Configuration Space Search

Complex reactive systems such as 5G cellular networks must have flexible configuration options to fit different deployment scenarios. However, not every possible configuration combination is risk-free. Some of them may lead to availability issues or even security vulnerabilities. Asking the system engineers to check each configuration via model checking for every deployment or re-configuration is impractical if not impossible. In this paper, we propose the concept of secure configuration space and develop a symbolic model checking algorithm, INCISE, to compute a large configuration space for a given reactive system. Such a space will be characterized by a logical condition (e.g., a Boolean formula). A system engineer can check any candidate configuration against the condition with a single SAT query to know whether it is secure. The target properties could be general safety and liveness properties. The algorithm enjoys the same benefits including efficiency and expressiveness as modern symbolic model checkers. We demonstrate the algorithm’s performance on industrial benchmarks and leverage it to address security issues in cellular network protocols.