SVSHI: Secure and Verified Smart Home Infrastructure

TL;DR

SVSHI is a platform that enhances the dependability of smart home systems by enabling formal verification and safe development of Python applications in KNX installations, improving reliability without sacrificing productivity.

Contribution

It introduces a novel platform combining AST manipulation, code generation, symbolic execution, and static verification for secure smart home application development.

Findings

Ensures application correctness and compatibility in KNX smart buildings.

Simplifies development of advanced smart home applications.

Provides formal guarantees of reliability and safety.

Abstract

Smart infrastructures uses are growing and with them the need for dependability and correctness. To provide better correctness guarantees and bring formal verification into the equation, we present SVSHI, a platform for developing, verifying, and running Python applications in KNX installations, one of the most used smart buildings standards. SVSHI leverages abstract syntax tree (AST) manipulation, code generation, symbolic execution, and static configuration verification to make writing advanced apps easy, quick, and safe. With SVSHI, the reliability and compatibility of the applications are guaranteed without foregoing users' productivity.