Development of Automated Tools for Solving CTFs

Motivation

IT Security is relevant in all parts of our every-day infrastructure. Therefore, protecting critical IT systems against unintential access by malicious actors becomes more important every day. Understanding attack vectors is prerequisite to protect systems effectively. Security experts can only create defenses against attacks by thinking like an attacker. A popular approach in the security community is to solve capture the flag (CTF) challenges, where an expert attempts to attack a specially designed system to gain access to, e.g., system files.

Goal and Method

Increasingly, tools using formal methods are employed in industry to automatically detect security vulnerabilities. The goal of the project was to develop CTF challenges that could be solved both manually and automatically using formal methods. The challenges could then serve to educate people on both the vulnerability and the formal method used to exploit it. To achive this goal, the project members identified security vulnerabilities amenable to automated exploits, tools to automate exploits based on (semi-)formal methods as well as existing secutity research tools, and demonstrated the viability of the approach by successfully solving the CTF challenges automatically, generating a description of the attack that could then be used to address the discovered issues.

Material

• Project Proposal and Description
• Short Introduction Slides (Joint Presentations)
• Extended Introduction Slides (Detailed Presentation)