SVSHI - Secure and Verified Smart Home Infrastructure
- SVSHI - Secure and Verified Smart Home Infrastructure
The SVSHI (Secure and Verified Smart Home Infrastructure) (pronounced like "sushi") project is a platform/runtime/toolchain for developing and running formally verified smart infrastructures, such as smart buildings, smart cities, etc.
It provides a CLI, svshi, to interact easily with the platform.
With SVSHI, a user can develop and run Python applications interacting with KNX systems that are formally verified at both compile and run-time against a set of provided invariants.
Installation
To work, SVSHI needs Python 3.9 (or newer)(download here), pip (pip will be automatically installed by scripts on Windows, on Linux simply use sudo apt install python3-pip and on MacOS use python3 -m ensurepip) and Java 11 (or newer)(download here). Optionally, sbt 1.5.5 (or newer) is needed to build from sources.
To check if the installation was successful, run svshi version in your terminal.
From archive
Unix (Linux / macOS)
To install SVSHI on Linux or macOS:
- Download the latest version
.zipfile from the Releases page - Unzip it, move the folder to the desired installation site, then run
./install.shinside it. - Add
$HOME/local/bin(where the CLI executable is stored) to the path by addingexport PATH=$HOME/local/bin:$PATHto your.bash_profile,.zsh_profile, etc. - Add the variable
SVSHI_HOMEto your environment by addingexport SVSHI_HOME=path/to/the/svshi/folder(a path example is~/svshi-v1.1.0) to your.bash_profile,.zsh_profile, etc.
To update SVSHI, you just need to do the first two steps. However, do not forget to reinstall the applications (stored in installedApps) by moving all the installedApps content in the new version's generated folder and compiling.
Windows
To install SVSHI on Windows:
- Download the latest version
.zipfile from the Releases page - Unzip the archive, move the unzipped folder to the desired installation site. The moved folder must contain (among other things) a
srcfolder and some scripts. - Open a Powershell instance a
CDinto the unzipped directory. - Setup
python3by executing the script.\setup-python3.ps1. This sets up apython3alias if it does not exist.The command
py,pythonorpython3must be available in your Powershell environment for this script to work! - Reboot your computer.
- Execute
.\install-pip.ps1to install pip on your computer - Run the
.\install.ps1script inside the unzipped folder to install the program.
IMPORTANT! use Powershell to execute the scripts!
To update SVSHI, you just need to do steps 1, 2, 3 and 7. However, do not forget to reinstall the applications (stored in installedApps) by moving all the installedApps content in the new version's generated folder and compiling.
From sources
Unix (Linux / macOS)
To build from sources on Linux or macOS:
- Clone the repository
- Run
./build.sh - Add
$HOME/local/bin(where the CLI executable is stored) to the path by addingexport PATH=$HOME/local/bin:$PATHto your.bash_profile,.zsh_profile, etc. - Add the variable
SVSHI_HOMEto your environment by addingexport SVSHI_HOME=path/to/your/cloned/repoto your.bash_profile,.zsh_profile, etc.
To update SVSHI, you just need to pull the latest changes and perform step 2. However, do not forget to reinstall the applications (stored in installedApps) by moving all the installedApps content in the new version's generated folder and compiling.
Windows
To build from sources on Windows:
- Clone the repository
- Open a Powershell instance and
CDinto the unzipped directory. - Setup
python3by executing the script.\setup-python3.ps1. This sets up apython3alias if it does not exist.The command
py,pythonorpython3must be available in your Powershell environment for this script to work! - Reboot your computer.
- Execute
.\install-pip.ps1to install pip on your computer - Run the
.\install.ps1 -build $truescript inside the cloned folder to install the program.
IMPORTANT! use Powershell to execute the scripts!
To update SVSHI, you just need to pull the latest changes and perform steps 2 and 6. However, do not forget to reinstall the applications (stored in installedApps) by moving all the installedApps content in the new version's generated folder and compiling.
Docker
We also provide a Docker image with all requirements and SVSHI installed. To use it:
- Run
./build_docker.shto build the image - Run
./run_docker.shto run the docker container. It opens ashinstance in the container with the current directory mapped to/pwdin the container - You can find the repo copied in
/home/maki/svshi svshicommand is accessible
Supported devices
- Binary sensors (deviceType = "binary")
- Temperature sensors (deviceType = "temperature")
- Humidity sensors (deviceType = "humidity")
- CO2 sensors (deviceType = "co2")
- Switches (deviceType = "switch")
Developing an application
To develop an app for SVSHI:
- Create the devices prototypical structure file containing the list of the devices the app should use, as explained in the app prototypical structure section.
- Run the app generator, as explained in the app generator section, to get the app skeleton. It will be created under the
generated/folder. - Write your app.
- Run
svshito generate the bindings withsvshi generateBindings -f ets.knxproj, where the argument is the absolute path to the ETS project file. - Map the right physical ids given in
generated/physical_structure.jsonto the right device ingenerated/apps_bindings.json. This is needed to provide the devices in the Python code with the group addresses to use. The first file represents the physical structure from the ETS project file, where each communication object has an id. The second one represents the apps structure with the devices and for each of them, the links they need. - Run
svshiagain to compile and verify the app withsvshi compile -f ets.knxproj.
Writing apps
To write an app, you mainly have to modify the main.py file, optionally adding dependencies into the requirements.txt file provided in the generated project. To understand how the project is generated, please refer to the app generation section.
All the available device instances are already imported in main.py. They mirror what has been defined in the device prototypical structure file.
The application can use external files. They however need to have been declared in the prototypical structure json file and they have to be located at the root of the project, next to main.py.
There are two important functions in main.py, invariant() and iteration(). In the first one the user should define all the conditions (or invariants) that the entire KNX system must satisfy throughout execution of all applications, while in the second she should write the app code.
An important thing to be aware of is that iteration() cannot use external libraries directly. Instead, these calls have to be defined first inside unchecked functions, which are functions whose name starts with unchecked and whose return type is explicitly stated. Then, these functions can be used in iteration().
In addition, note that invariant() must return a boolean value, so any kind of boolean expression containing the read properties of the devices and constants is fine. However, here operations with side effects, external libraries calls and unchecked functions calls are not allowed.
Unchecked functions are used as a compromise between usability and formal verification, and as such must be used as little as possible: their content is not verified by SVSHI. Furthermore, they should be short and simple: we encourage developers to add one different unchecked function for each call to an external library. All logic that does not involve calls to the library should be done in iteration() to maximize code that is indeed formally verified. Nonetheless, the user can help the verification deal with their presence by annotating their docstring with post-conditions.
Functions' post-conditions define a set of axioms on the return value of the function: these conditions are assumed to be always true by SVSHI during verification. They are defined like this: post: __return__ > 0. You can use constants and other operations. You can add as much post-conditions as you like and need. Therefore, we encourage developers to avoid having conjunctions in post-conditions but rather to have multiple post-conditions. This does not make difference for the verification but helps the readability.
However, keep in mind that these conditions are assumed to be true during formal verification! If these do not necessarily hold with respect to the external call, bad results can occur at runtime even though the code verification was successful!
An example with multiple post-conditions could be:
def unchecked_function() -> int:
"""
post: __return__ > 0
post: __return__ != 3
"""
return external_library_get_int()
Furthermore, applications have access to a set of variables (the app state) they can use to keep track of state between calls. Indeed, the iteration() function is called in an event-based manner (either the KNX devices' state changes or a periodic app's timer is finished). All calls to iteration() are independent and thus SVSHI offers a way to store some state that will live in between calls. There is a local state instance per app.
To do so, in main.py the app_state instance is imported along with the devices. This is a dataclass and it contains 4 fields of each of the following types: int, float, bool and str. The fields are called respectively INT_X, FLOAT_X, BOOL_X and STR_X where X equals 0, 1, 2 or 3.
These values can be used in iteration() and invariant(). One should be careful while using it in invariant() or in a condition that will affect the KNX installation's state (the physical state): the formal verification would fail if ANY possible value of the app_state leads to an invalid state after running iteration() even if this case should not occur because of previous calls to iteration() that would have set the values.
App example
In main.py:
from instances import app_state, BINARY_SENSOR, SWITCH
def invariant() -> bool:
# The switch should be on when the binary sensor is on or when INT_0 == 42, off otherwise
return ((BINARY_SENSOR.is_on() or app_state.INT_0 == 42) and SWITCH.is_on()) or (not BINARY_SENSOR.is_on() and not SWITCH.is_on())
def iteration():
if BINARY_SENSOR.is_on() or app_state.INT_0 == 42:
SWITCH.on()
else:
SWITCH.off()
Running the applications
To run all the installed apps (with runtime verification enabled):
- In ETS, import the file
assignments/assignment.csvto create the group addresses, then assign to each communication object the right group address as presented inassignments/assignment.txt. The name of the group address should help understanding which device it is meant to. - In ETS, do a basic configuration of the devices to make them have the correct basic behaviour (the amount of configuration depends on the particular device)
- Execute
svshi run -a address:port, where address is the KNX IP gateway address and port is the KNX IP gateway port.
SVSHI logs which apps have been called during execution and which telegrams have been received. You can find the logs in logs/.
Updating an application
If you want to update the code of an app that is already installed, SVSHI offers a simplified process. To be updated, an app must have the same prototypical structure as its previous version and be installed.
To update the app, you then:
- Put the new version of the app in the
generatedfolderThere must be NO other app in the folder
- Run
svshi updateApp -n app_namewhereapp_nameis the app you want to update
Using this process, you do not need to generate or modify the bindings and you do not need to pass an ETS project.
If the new version does not pass the verification stage, the update is aborted and the old set of apps is restored as before the operation.
App generator
Prototypical structure
This JSON file is given by the programmer/developer that wants to develop an application. It represents the prototypical devices that the app needs with their types. It also specifies whether the app is privileged or not ("permissionLevel": "privileged" | "notPrivileged"). A privileged app overrides the behavior of the non-privileged ones at runtime.
Moreover, the timer attribute can be used to run the application even though the physical state has not changed. The app thus becomes a periodic app.
- If
timer == 0the application runs only when the physical state of the devices it uses changes - If
timer > 0the application runs when the physical state changes AND everytimerseconds.
The files attributes is used to indicate files that the app needs to work properly. These files must be at the root of the application project (next to main.py).
Once the app is generated, it is moved in the generated apps' folder.
Here is an example:
{
"permissionLevel": "notPrivileged",
"timer": 60,
"files": ["file1.txt", "file2.png"],
"devices": [
{
"name": "name_of_the_instances",
"deviceType": "type_of_the_devices"
}
]
}
The name is used as the instance name in the Python app that is generated. It should then be unique in a given app, and should follow the Python variables naming conventions: no whitespaces nor numbers. The deviceType should be supported by SVSHI.
Usage
The app generator takes as input the devices JSON file and the name of the app.
Before executing it, you need to create the file containing the list of the devices the app should use, as explained above.
To execute the generator, run svshi generateApp -d devices.json -n app_name, where the first argument is the absolute path to the prototypical structure file and the second one (app_name in the example) is the name of the app to be used. The name has to follow the same rules as for Python modules: short, all-lowercase names. Underscores can be used if it improves readability.
CLI
You can run svshi --help to display the following:
svshi
Secure and Verified Smart Home Infrastructure
task The task to run. Can be passed as is. Possible options are 'run', 'compile', 'generateBindings', 'generateApp', 'removeApp', 'listApps' and 'version'. This argument is not case sensitive.
-f --ets-file
The ETS project file to use for the tasks 'compile' and 'generateBindings'
-d --devices-json
The devices prototypical structure JSON file to use for the task 'generateApp'
-n --app-name
The app name to use for the tasks 'generateApp' and 'removeApp'
-a --address
The KNX address to use for the task 'run'. The correct format is 'address:port' (ex: 192.168.1.1:5555)
--no-colors The flag to disable output coloring
--all The flag to remove all apps for the task 'removeApp'
Available commands are:
svshi run -a 1.1.1.1:5555to run all the apps with runtime verificationsvshi compile -f ets.knxprojto compile all the appssvshi generateBindings -f ets.knxprojto generate the bindings for all the appssvshi generateApp -d devices.json -n app_nameto generate a new Python appsvshi removeApp -n app_nameto remove an installed appsvshi updateApp -n app_nameto update the code of an app that is already installedsvshi listAppsto list all the installed appssvshi versionto display the CLI version
Shorter aliases are also available:
svshi rforsvshi runsvshi cforsvshi compilesvshi gbforsvshi generateBindingssvshi gaforsvshi generateAppsvshi raforsvshi removeAppsvshi uaforsvshi updateAppsvshi laforsvshi listAppssvshi vforsvshi version
How SVSHI works
Compilation
The compiler combines all applications already installed (in app_library) with new applications (in generated). It generates the bindings between physical and prototypical devices communication objects, assigns group addresses to used physical communication objects and produces useful files for the runtime.
When compiling applications, if the verification passed all checks, applications from generated are moved into app_library to become installed applications.
Bindings
The compiler generates the bindings file to let the developer map physical device communication objects (from the ETS project) to prototypical devices from applications.
Bindings for the installed applications are stored and when svshi generateBindings -f ets.knxproj is called, the new bindings reuse current bindings if the physical structure did not change since last application installation. Therefore, only bindings for new applications are empty and must be filled. If the physical structure changed, the bindings file is a fresh one and all bindings must be entered again.
Verification
Static
When compiling, the apps are also verified to make sure each one of them satisfies the invariants of each app. If not, the procedure fails with helpful error messages. Therefore, the static verification not only catches apps violating the invariants, but it also ensures compatibility between installed apps.
Runtime
Whenever an app wants to update the KNX system, SVSHI verifies whether the update could break the apps' invariants. If it is the case, the app is prevented from running, otherwise the updates are propagated to KNX.
Execution
SVSHI's runtime is reactive and event-based. Applications listen for changes to the group addresses of the devices they use, and are run on a state change (an event). The state transition can be triggered externally by the KNX system or by another app, which then proceeds to notify all the other listeners. Notable exception are apps that run every X seconds based on a timer, which not only react to state changes but are also executed periodically.
Running an application concretely means that its iteration() function is executed on the current physical state of the system and on the current app state.
Apps are always run in alphabetical order in their group (privileged or notPrivileged). The non-privileged apps run first, then the privileged ones: in such a way privileged applications can override the behavior of non-privileged ones.
This execution model has been chosen for its ease of use: users do not need to write while loops or deal with synchronization explicitly.
KNX Virtual
You do not necessarily need to build a KNX infrastructure to test your app. You can use KNX Virtual to run SVSHI. This a Windows-only program that is available on the KNX Association's website1. Once you downloaded and installed it, you can use it exactly as a physical installation with SVSHI. Use the startup settings of KNX Virtual (address and port) when executing svshi run. Default values are 127.0.0.1:3671.
Please be careful and use the right devices inside ETS when configuring the project and refer to the KNX Help for KNX Virtual related issues2.
Contributing
See the contributing guide for detailed instructions on how to get started with the project.
White paper
See the white paper for an in-depth understanding about why SVSHI exists, what it does and how it does it.
License
SVSHI is licensed under the MIT license.
Logo: Copyright @norafisler
81 Nov 22, 2022
5 Jan 09, 2022
2 Apr 20, 2022
1 Mar 18, 2022
185 Dec 22, 2022
2 Jan 19, 2022
7 Oct 14, 2022
7 Apr 21, 2022
8 Jun 24, 2022
1 Jan 03, 2022
3 Nov 16, 2021
5 May 20, 2022
1 Jun 16, 2022
12.9k Jan 05, 2023
2 Oct 09, 2022
93 Oct 05, 2022
27 Jan 01, 2023
3 Dec 20, 2022
162 Dec 21, 2022