The new attack surface being crafted by the huge influx of IoT devices is both formidable and unpredictable, as it introduces a rich set of unexplored attack techniques and unknown vulnerabilities. These new attack techniques are hard to perceive through traditional means, owing to concealed and cascaded inter-device, inter-system and device-environment dependencies. In this paper, we present IoTSAT, a formal framework for security analysis of IoT. IoTSAT formally models the generic behavior of IoT system of systems, based on device configurations, network topologies, user policies and IoT-specific attack surface. The model is then used to measure system's resilience against potential attacks and identify threat vectors and specific attack techniques, which can be used to achieve higher-level adversary's objectives. We evaluate IoTSAT over realistic IoT networks, which concludes that our approach is scalable and highly beneficial for uncovering complex attack vectors of IoT systems.