mirror of
https://github.com/tiyn/wiki.git
synced 2026-01-10 08:39:45 +01:00
Compare commits
12 Commits
0e2428f56e
...
661ce3f20b
| Author | SHA1 | Date | |
|---|---|---|---|
| 661ce3f20b | |||
| 771ecc3b99 | |||
| d6c9c6fdae | |||
| 362aee2899 | |||
| 9f162704d1 | |||
| 4a91f12dcd | |||
| 380f9b34d7 | |||
| 2c48962955 | |||
| d7770d09d9 | |||
| b125fadd9c | |||
| 71abe3c423 | |||
| de74434cf3 |
@@ -94,7 +94,7 @@ This app is available at [F-Droid](/wiki/android/f-droid.md) as
|
||||
|
||||
## Custom ROMs
|
||||
|
||||
Besites the stock-firmware of vendors there are also custom ROMs.
|
||||
Besides the stock-firmware of vendors there are also custom ROMs.
|
||||
These are alternative firmware variants made by third party providers.
|
||||
A well known custom ROM is [LineageOS](/wiki/android/lineageos.md).
|
||||
|
||||
|
||||
@@ -38,6 +38,21 @@ Finally if a reverse proxy is used check the
|
||||
|
||||
Afterwards you're ready to go by once again running the `rebuild.sh` file.
|
||||
|
||||
If setting up this mailserver with [Traefik](/wiki/traefik.md) as a reverse proxy some additional
|
||||
steps should be taken.
|
||||
No http or https is needed.
|
||||
But a certificate for the mailserver is needed regardless.
|
||||
In this case add the following lines to the file `docker-compose.yml` in the
|
||||
`services:` section and adapt them.
|
||||
|
||||
```yml
|
||||
whoami:
|
||||
image: docker.io/traefik/whoami:latest
|
||||
labels:
|
||||
- "traefik.enable=true"
|
||||
- "traefik.http.routers.whoami.rule=Host(`<subdomain>.<domain>`)"
|
||||
```
|
||||
|
||||
### rebuild.sh
|
||||
|
||||
```sh
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
# traefik
|
||||
|
||||
This is a [Docker](/wiki/docker.md) container for a traefik edge router.
|
||||
This is a [Docker](/wiki/docker.md) container for a [Traefik](/wiki/traefik.md) edge router.
|
||||
The official container and documentation was made by
|
||||
[traefik](https://hub.docker.com/_/traefik).
|
||||
This docker-rebuild is made up by a `docker-compose.yml` file.
|
||||
@@ -12,6 +12,8 @@ In that folder create the directories `data/config`.
|
||||
Place the files `data/traefik.yml` and `data/config/dynamic.yml` in the
|
||||
according directories.
|
||||
Change the settings according to your needs and run `./rebuild.sh` afterwards.
|
||||
Additional guides on the usage of Traefik for [Docker](/wiki/docker.md) services can be found in
|
||||
the [Traefik wiki entry](/wiki/traefik.md#usage).
|
||||
|
||||
### Volumes
|
||||
|
||||
@@ -145,7 +147,7 @@ certificatesResolvers:
|
||||
|
||||
### data/config/dynamic.yml
|
||||
|
||||
In the config replace `username:htpasswd` with the output of
|
||||
In the config replace `<username:htpasswd>` with the output of
|
||||
`echo $(htpasswd -nb <user> <pasword>) | sed -e s/\\$/\\$\\$/g`.
|
||||
|
||||
```yml
|
||||
@@ -162,19 +164,7 @@ http:
|
||||
user-auth:
|
||||
basicAuth:
|
||||
users:
|
||||
- "username:htpasswd"
|
||||
|
||||
redirect-non-www-to-www:
|
||||
redirectregex:
|
||||
permanent: true
|
||||
regex: "^https?://(?:www\\.)?(.+)"
|
||||
replacement: "https://www.${1}"
|
||||
|
||||
redirect-www-to-non-www:
|
||||
redirectregex:
|
||||
permanent: true
|
||||
regex: "^https?://www\\.(.+)"
|
||||
replacement: "https://${1}"
|
||||
- "<username:htpasswd>"
|
||||
|
||||
tls:
|
||||
options:
|
||||
@@ -188,73 +178,3 @@ tls:
|
||||
- TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305
|
||||
minVersion: VersionTLS12
|
||||
```
|
||||
|
||||
The sections called `redirect-non-www-to-www` and `redirect-www-to-non-www` are adapted from a
|
||||
article by Benjamin Rancourt on his
|
||||
[website](https://www.benjaminrancourt.ca/how-to-redirect-from-non-www-to-www-with-traefik/).
|
||||
|
||||
## Usage
|
||||
|
||||
### Create reverse proxies
|
||||
|
||||
To create a reverse proxy from a docker container add the following lines in the
|
||||
`labels:` section of the `docker-compose.yml` of the service to proxy.
|
||||
|
||||
```yml
|
||||
- "traefik.enable=true"
|
||||
- "traefik.docker.network=proxy"
|
||||
- "traefik.http.routers.<service name>-secure.entrypoints=websecure"
|
||||
- "traefik.http.routers.<service name>-secure.rule=Host(`<subdomain>.<domain>`)"
|
||||
- "traefik.http.routers.<service name>-secure.service=<service name>"
|
||||
- "traefik.http.services.<service name>.loadbalancer.server.port=<port>"
|
||||
```
|
||||
|
||||
This configuration automatically redirects http to https.
|
||||
When using this configuration the port specified in the latter lines can be
|
||||
ommitted in the `ports:` section if not used directly.
|
||||
This ensures access only via https and restricts access via ip and port.
|
||||
Change `<service name>` according to the service you want to publish and `<subdomain>` aswell as
|
||||
`<domain>` to the domain you intent to publish the service to.
|
||||
Additionally if you want to redirect domains not starting with `www` to one that does not append
|
||||
the following line.
|
||||
|
||||
```yml
|
||||
- "traefik.http.routers.<service name>.middlewares=redirect-non-www-to-www"
|
||||
```
|
||||
|
||||
If the opposite is the case and it should always be redirected to a domain not starting with `www`
|
||||
add the following line.
|
||||
|
||||
```yml
|
||||
- "traefik.http.routers.<service name>.middlewares=redirect-www-to-non-www"
|
||||
```
|
||||
|
||||
In both of those cases the line of the first code block in this section that specifies the domain
|
||||
and subdomain needs to include both the www and the non-www domains.
|
||||
This should look something like the following
|
||||
|
||||
Make sure to add the domain that will be redirected to the labels aswell.
|
||||
For redirection to www domains this will look something like the following.
|
||||
|
||||
```yml
|
||||
- "traefik.http.routers.<service name>.rule=Host(`<subdomain>.<domain>`)"
|
||||
```
|
||||
|
||||
In the opposite case the domain will be `www.<subdomain>.<domain>`.
|
||||
|
||||
### Setup Mailserver
|
||||
|
||||
If setting up a
|
||||
[docker-mailserver by mailserver](./mailserver_-_docker-mailserver.md) no http
|
||||
or https is needed.
|
||||
But a certificate for the mailserver is needed regardless.
|
||||
In this case add the following lines to the file `docker-compose.yml` in the
|
||||
`services:` section and adapt them.
|
||||
|
||||
```yml
|
||||
whoami:
|
||||
image: docker.io/traefik/whoami:latest
|
||||
labels:
|
||||
- "traefik.enable=true"
|
||||
- "traefik.http.routers.whoami.rule=Host(`<subdomain>.<domain>`)"
|
||||
```
|
||||
|
||||
37
wiki/docker/viperproject_-_viperserver.md
Normal file
37
wiki/docker/viperproject_-_viperserver.md
Normal file
@@ -0,0 +1,37 @@
|
||||
# viperproject - viperserver
|
||||
|
||||
This is a [Docker](/wiki/docker.md) container for a [Viper](/wiki/programming_language/viper.md)
|
||||
server, which is used for building the Viper verifiers
|
||||
[Silicon and Carbon](/wiki/programming_language/viper.md#setup).
|
||||
The official container and documentation was made by
|
||||
[viperproject](https://hub.docker.com/r/viperproject/viperserver).
|
||||
|
||||
## Set-up
|
||||
|
||||
Create the file `rebuild.sh`.
|
||||
Change the settings according to your needs and run `./rebuild.sh` afterwards.
|
||||
Due to this container being used to build the Silicon and Carbon verifiers it is recommended to be
|
||||
started in interactive mode as demonstrated in the [rebuild section](#rebuildsh).
|
||||
Make sure to substitute `<path-to-carbon>` and `<path-to-silicon>`.
|
||||
If only one of them is to be built, omit the other.
|
||||
Additionally the version of viperproject has to be added for `<viperproject-version>`.
|
||||
It also depends on the Z3 version which will be used later.
|
||||
For example the version `v4_z3_4.8.7` is working for Z3 versions `4.8.7` and later.
|
||||
|
||||
## Volumes
|
||||
|
||||
Set the following volumes with the -v tag.
|
||||
|
||||
| Outside mount/volume name | Container mount | Description |
|
||||
| ------------------------- | --------------- | ----------------------------------------- |
|
||||
| `<path-to-silicon>` | `/mnt/silicon` | (optional) mount Silicon for installation |
|
||||
| `<path-to-carbon>` | `/mnt/carbon` | (optional) mount Carbon for installation |
|
||||
|
||||
## rebuild.sh
|
||||
|
||||
```sh
|
||||
docker run -it --name viperserver \
|
||||
-v <path-to-silicon>:/mnt/silicon \
|
||||
-v <path-to-carbon>:/mnt/carbon \
|
||||
viperproject/viperserver:<viperproject-version>
|
||||
```
|
||||
@@ -48,12 +48,13 @@ git ls-files -v | grep "^S"
|
||||
Authentication by default is done via a username and a password.
|
||||
For some services such as GitHub.
|
||||
it is not possible to use password as an authentication method.
|
||||
The other possibility to authenticate to git is by using
|
||||
[SSH](/wiki/linux/ssh.md).
|
||||
The other possibility to authenticate to git is by using [SSH](/wiki/ssh.md).
|
||||
|
||||
The following sections assumes using a [Linux-based system](/wiki/linux.md) using
|
||||
[OpenSSH](/wiki/linux/openssh.md).
|
||||
For this a
|
||||
[SSH certificate has to be created](/wiki/linux/ssh.md#generate-new-keys) and
|
||||
[added to the authentication agent](/wiki/linux/ssh.md#adding-keys-to-authentication-agent).
|
||||
[SSH certificate has to be created](/wiki/linux/openssh.md#generate-new-keys) and
|
||||
[added to the authentication agent](/wiki/linux/openssh.md#adding-keys-to-authentication-agent).
|
||||
Afterwards it the public SSH key to be added to the git server.
|
||||
For GitHub there is
|
||||
[a guide on that topic](https://docs.github.com/en/get-started/getting-started-with-git/why-is-git-always-asking-for-my-password).
|
||||
@@ -71,16 +72,52 @@ git clone https://github.com/tiyn/wiki
|
||||
By using the SSH config file the clone command can be shortened to
|
||||
`git clone github:tiyn/wiki`.
|
||||
For this follow the
|
||||
[corresponding section in the SSH entry](/wiki/linux/ssh.md#shorten-ssh-connection-commands).
|
||||
[corresponding section in the SSH entry](/wiki/linux/openssh.md#shorten-ssh-connection-commands).
|
||||
Set `Host` to `github`, `HostName` to `github.com` and `User` to `git`.
|
||||
|
||||
### Improved `git diff`
|
||||
|
||||
[Diff So Fancy](https://github.com/so-fancy/diff-so-fancy) is a drop in
|
||||
replacement for the default `git diff` look.
|
||||
It can be installed via the
|
||||
[repository](https://github.com/so-fancy/diff-so-fancy) or the `diff-so-fancy`
|
||||
package.
|
||||
There are different possibilities to improve the diff of git.
|
||||
One of them is [diff-so-fancy](#git-diff-diff-so-fancy) which allows word specific `git diff`.
|
||||
A second and more modern option is [delta](#git-diff-delta) which additionally allows syntax
|
||||
highlighting and a side-by-side view.
|
||||
delta also improves the `git blame` command, which is another reason why it is widely more popular
|
||||
then diff-so-fancy.
|
||||
|
||||
A more or less complete overview of the options was performed in an
|
||||
[Article on Medium by Maxim Smolin](https://maximsmol.medium.com/improving-git-diffs-4519a6541cd1).
|
||||
|
||||
#### `git diff`: Delta
|
||||
|
||||
[delta](https://github.com/dandavison/delta) first needs to be installed.
|
||||
Most [package managers](/wiki/linux/package_manager.md) package it in the package `git-delta`.
|
||||
|
||||
Afterwards it needs to be enabled.
|
||||
To do this globally add the following lines to the configuration file of git, which can be found in
|
||||
`~/.gitconfig`.
|
||||
Depending on the system settings and preferences the dark-mode (`dark`) and the side-by-side view
|
||||
(`side-by-side`) can and should be disabled.
|
||||
|
||||
```txt
|
||||
[core]
|
||||
pager = delta
|
||||
[interactive]
|
||||
diffFilter = delta --color-only
|
||||
[delta]
|
||||
navigate = true
|
||||
dark = true
|
||||
side-by-side = true
|
||||
show-syntax-themes = true
|
||||
[merge]
|
||||
conflictStyle = zdiff3
|
||||
```
|
||||
|
||||
#### `git diff`: diff-so-fancy
|
||||
|
||||
[diff-so-fancy](https://github.com/so-fancy/diff-so-fancy) is a drop in replacement for the default
|
||||
`git diff` look.
|
||||
It can be installed via most [package managers](/wiki/linux/package_manager.md) using the
|
||||
`diff-so-fancy` package.
|
||||
Afterwards the following lines need to be run to complete the configuration.
|
||||
|
||||
```sh
|
||||
|
||||
@@ -175,5 +175,9 @@ password-border-radius = 0.341125em
|
||||
|
||||
## Troubleshooting
|
||||
|
||||
This section will focus on errors and the fixing of errors of LightDM.
|
||||
|
||||
### Bypass LightDM on Error
|
||||
|
||||
If it comes to problems that deny the login it can be useful to switch to another tty.
|
||||
This can be done by hitting the key combination `CTRL+ALT+F2`.
|
||||
|
||||
@@ -1,14 +1,17 @@
|
||||
# SSH
|
||||
# OpenSSH
|
||||
|
||||
SSH is a network protocoll to securely connect to a computer.
|
||||
In this article it is assumed that `openssh` is used.
|
||||
[OpenSSH](https://www.openssh.com) is an implementation of the [SSH protocol](/wiki/ssh.md).
|
||||
|
||||
## Usage
|
||||
|
||||
This section addresses the usage of OpenSSH.
|
||||
|
||||
### Generate New Keys
|
||||
|
||||
To generate new ssh keys simply run `ssh-keygen -t ed25519` or
|
||||
`ssh-keygen -t rsa -b 4096`.
|
||||
For security reasons the Ed25519 is more secure, even if the key length is far smaller than its RSA
|
||||
counterpart.
|
||||
|
||||
The keys can then be added to the authentication agent by as described in the
|
||||
[corresponding article](#adding-keys-to-authentication-agent)
|
||||
@@ -35,15 +38,30 @@ to `PermitRootLogin yes`.
|
||||
To enable easy login without password you can add the contents of the file
|
||||
`~/.ssh/id_rsa.pub` from your local machine to the file `~/.ssh/authorized_keys`
|
||||
on the machine you want to log into.
|
||||
You can use the modified command below for ease of use:
|
||||
|
||||
There are two options to add the public key to the remote machine.
|
||||
The first is a more manual approach.
|
||||
`<path-to-public-key>` is the path to the public key (for example `~/.ssh/id_rsa.pub`) and `<host>`
|
||||
is the (user and) server to add the key to (for example `user@192.168.178.16`).
|
||||
|
||||
```sh
|
||||
cat ~/.ssh/id_rsa.pub | ssh username@server 'cat >> ~/.ssh/authorized_keys'
|
||||
cat <path-to-public-key> | ssh <host> 'cat >> ~/.ssh/authorized_keys'
|
||||
```
|
||||
|
||||
This can also be more or less fully automated using the `-G` flag of SSH as described in
|
||||
This can also be more or less fully automated using the `-G` flag of SSH as described in
|
||||
[a YouTube video by nixhero](https://www.youtube.com/watch?v=xCX14u9XzE8).
|
||||
|
||||
The second option is a bit safer, due to using OpenSSHs tools, was described in a
|
||||
[StackOverflow comment by Boy](https://stackoverflow.com/questions/18690691/how-to-add-a-ssh-key-to-remote-server).
|
||||
It functions similar to the first and uses the following command.
|
||||
|
||||
```sh
|
||||
ssh-copy-id -f -i <path-to-public-key> <host>
|
||||
```
|
||||
|
||||
The `-f` flag can alos be omittet to check if the key is already installed.
|
||||
For being very safe is important, a dry run can be performed using the `-n` flag.
|
||||
|
||||
### Mount Directory With SSHFS
|
||||
|
||||
This section is loosely based on
|
||||
@@ -157,3 +175,18 @@ kill <process-id>
|
||||
|
||||
Files that are based on a remote server can be mounted as described in
|
||||
[the corresponding section](#mount-directory-with-sshfs) to setup complete remote development.
|
||||
|
||||
### Specify Key Exchange Algorithms
|
||||
|
||||
It can be useful to specify the key exchange algorithms in the OpenSSH config file `~/.ssh/config`.
|
||||
Some key exchange algorithms are more secure regarding post-quantum attacks.
|
||||
The following configuration prefers and enforces hybrid post-quantum–resistant key exchange
|
||||
algorithms (`mlkem768x25519-sha256` and `sntrup761x25519-sha512`).
|
||||
A modern classical fallback (`curve25519-sha256`) is included for compatibility.
|
||||
This can be considered a form on
|
||||
[system hardening](/wiki/linux/system-hardening.md#specific-steps-to-harden-a-system).
|
||||
|
||||
```
|
||||
Host *
|
||||
KexAlgorithms mlkem768x25519-sha256,sntrup761x25519-sha512,curve25519-sha256
|
||||
```
|
||||
58
wiki/linux/raspberry_pi.md
Normal file
58
wiki/linux/raspberry_pi.md
Normal file
@@ -0,0 +1,58 @@
|
||||
# Raspberry Pi
|
||||
|
||||
A [Rapberry Pi](https://www.raspberrypi.com) is a single board comuter.
|
||||
|
||||
## Hardware Additions
|
||||
|
||||
There are various hardware additions which can be used with the Raspberry Pi.
|
||||
This section addresses them.
|
||||
|
||||
### AI HAT+
|
||||
|
||||
The [AI HAT](https://www.raspberrypi.com/documentation/accessories/ai-hat-plus.html) is an
|
||||
extension which uses the Hailo AI module for use with the [Raspberry Pi
|
||||
5](https://www.raspberrypi.com/products/raspberry-pi-5).
|
||||
|
||||
#### AI HAT+ Usage
|
||||
|
||||
This section addresses the usage of the
|
||||
[AI HAT](https://www.raspberrypi.com/documentation/accessories/ai-hat-plus.html).
|
||||
|
||||
#### Preparing TensorFlow Models for the AI HAT+
|
||||
|
||||
For neural networks to run on the Hailo AI module and the AI HAT+ they have to be converted to the
|
||||
`.hef` format.
|
||||
This section assumes the neural network is using
|
||||
[TensorFlow](/wiki/programming_language/python.md#tensorflow) and is available as a `.tf` or
|
||||
`.tflite` file.
|
||||
|
||||
To convert TensorFlow models first the Hailo 8 Software Suite needs to be downloaded.
|
||||
This can be done from the [official website](https://hailo.ai/developer-zone/software-downloads/)
|
||||
altough an account is needed for it.
|
||||
|
||||
After downloading, extracting and then navigating into the folder a heavily customized
|
||||
[Docker](/wiki/docker.md) container can be started by running the following command.
|
||||
However it is recommended to slightly modify this file.
|
||||
Add a volume that contains the TensorFlow model, that is to be converted, to the environment
|
||||
variable `DOCKER_ARGS` which is set in the file `hailo_ai_sw_suite_docker_run.sh`.
|
||||
|
||||
```sh
|
||||
./hailo_ai_sw_suite_docker_run.sh
|
||||
```
|
||||
|
||||
Using the tools which come in this container a `.tf` or `.tflite` model can be converted to the
|
||||
`.hef` format.
|
||||
|
||||
For this to work run the following commands inside the Docker container.
|
||||
The first command takes the path to the tensorflow model (`<path-to-tf-model>`) and will output a
|
||||
`.har` model.
|
||||
The second command is optional but recommended and takes the path to this `.har` model
|
||||
(`<path-to-har-model`) and returns an optimized `.har` model.
|
||||
The third and final command compiles the (optimized) `.har` model, which is given as the input, and
|
||||
outputs the final `.hre` model, which then can be used with the Hailo AI module.
|
||||
|
||||
```sh
|
||||
hailo parser tf <path-to-tf-model>
|
||||
hailo optimize --use-random-calib-set <path-to-har-model>
|
||||
hailo compiler <path-to-optimized-har-model>
|
||||
```
|
||||
@@ -10,3 +10,12 @@ data.
|
||||
list of security flaws of your system
|
||||
- [arch-audit](https://gitlab.archlinux.org/archlinux/arch-audit) is a tool to find vulnerabilities
|
||||
known to the [Arch](/wiki/linux/arch-linux.md) Security Team.
|
||||
|
||||
## Specific Steps to Harden a System
|
||||
|
||||
The following points are steps that harden a system.
|
||||
|
||||
- For [OpenSSH](/wiki/linux/openssh.md) enable hybrid post-quantum key exchange algorithms as
|
||||
described in the [corresponding entry](/wiki/linux/openssh.md#specify-key-exchange-algorithms).
|
||||
Using hybrid post-quantum-safe key exchange methods reduces the risk of so called "store-now,
|
||||
decrypt-later" attacks.
|
||||
|
||||
@@ -15,3 +15,13 @@ For this to work the compositor needs to use wlroots.
|
||||
```sh
|
||||
wlr-randr
|
||||
```
|
||||
|
||||
## Troubleshooting
|
||||
|
||||
This section addresses problems that can occur when using Wayland and ways to solve them.
|
||||
|
||||
### Invisible Notifications and Pop-Ups
|
||||
|
||||
There is a chance that notifications and pop-ups are not displayed correctly at some time when
|
||||
using Wayland.
|
||||
To fix this the most simple way is to just restart the compositor that is currently used.
|
||||
|
||||
@@ -10,7 +10,7 @@ To setup a Meshtastic Node a device that is capable of communicating via LoRa is
|
||||
Often used devices are [microcontrollers](/wiki/microcontroller.md) based on the
|
||||
[ESP32-chip](/wiki/microcontroller.md#esp32) like the LILYGO TTGO T-BEAM or the Heltec V3, devices
|
||||
based on the nRF52-chip like the RAK4631 and the LILYGO TTGO T-Echo or devices based on the
|
||||
RP2040-chip like the Raspberry Pi Pico or the RAK11310 are needed.
|
||||
RP2040-chip like the [Raspberry Pi](/wiki/linux/raspberry_pi.md) Pico or the RAK11310 are needed.
|
||||
|
||||
After the device acquisition the meshtastic firmware needs to be flashed on the device.
|
||||
This can be done using the [official Meshtastic Web Flasher](https://flasher.meshtastic.org/).
|
||||
|
||||
87
wiki/programming_language/viper.md
Normal file
87
wiki/programming_language/viper.md
Normal file
@@ -0,0 +1,87 @@
|
||||
# Viper
|
||||
|
||||
[Viper](https://www.pm.inf.ethz.ch/research/viper.html) is a verification language among other
|
||||
tools.
|
||||
|
||||
## Setup
|
||||
|
||||
For the Viper language to work a verifier needs to be set up.
|
||||
The two possibilities are [Carbon](https://github.com/viperproject/carbon) and
|
||||
[Silicon](https://github.com/viperproject/silicon).
|
||||
|
||||
This section explains the installation for [Linux-based systems](/wiki/linux.md), but they are also
|
||||
available for [Windows](/wiki/windows.md) systems though the steps to setup differ.
|
||||
For this navigate download the code from [Silicons Github](https://github.com/viperproject/silicon)
|
||||
and/or [Carbon Github](https://github.com/viperproject/carbon).
|
||||
|
||||
There are some dependencies.
|
||||
For both Carbon and Silicon to work correctly Z3 has to be installed.
|
||||
This can easily be done, for example by installing the `z3` package, which is available from
|
||||
various [package managers](/wiki/linux/package_manager/pacman_and_aur.md).
|
||||
For Carbon Boogie has to be installed too.
|
||||
This is best done by installing a .NET SDK which is often packaged in a package called `dotnet-sdk`
|
||||
or a similar named one.
|
||||
Afterwards boogie can be installed using the following command.
|
||||
|
||||
```sh
|
||||
dotnet tool install -g boogie
|
||||
```
|
||||
|
||||
Afterwards the building of Silicon and/or Carbon can follow.
|
||||
|
||||
The easiest way to build one or both verifiers locally is creating a `.jar` file via
|
||||
[Docker](/wiki/docker.md) using the
|
||||
[viperproject image](/wiki/docker/viperproject_-_viperserver.md).
|
||||
|
||||
Start the Docker container as explained in the
|
||||
[corresponding wiki entry](/wiki/docker/viperproject_-_viperserver.md).
|
||||
Make sure to change the setting as described.
|
||||
Then in the Docker container build Silicon by running the following commands.
|
||||
|
||||
```sh
|
||||
cd /mnt/silicon
|
||||
sbt assembly
|
||||
```
|
||||
|
||||
For Carbon similarly run the following commands.
|
||||
|
||||
```sh
|
||||
cd /mnt/carbon
|
||||
sbt assembly
|
||||
```
|
||||
|
||||
Afterwards leave the Docker container.
|
||||
It is no longer needed.
|
||||
|
||||
The `.jar` files are now available in `<path-to-carbon>/target/scala-<version>/carbon.jar` or
|
||||
`<path-to-silicon>/target/scala-2.13/silicon.jar` and are ready to be used outside the docker
|
||||
container from the host machine.
|
||||
|
||||
Afterwards Carbon and/or Silicon are ready to be [used](#usage).
|
||||
|
||||
## Usage
|
||||
|
||||
This section addresses the usage of Viper.
|
||||
|
||||
### Basic Verifier Usage
|
||||
|
||||
After [Silicon](https://github.com/viperproject/silicon) and/or
|
||||
[Carbon](https://github.com/viperproject/carbon) have been setup according to the
|
||||
[setup section](#setup), they can be used.
|
||||
|
||||
For Silicon run the following command.
|
||||
`<path-to-silicon-jar>` describes the path of the Silicon jar which was set in the [setup](#setup).
|
||||
`<path-to-viper-file>` is the path to the Viper file to verify.
|
||||
|
||||
```sh
|
||||
java -jar <path-to-silicon-jar> <path-to-viper-file>
|
||||
```
|
||||
|
||||
For Carbon run the following command.
|
||||
`<path-to-carbon-jar>` describes the path of the Carbon jar which was set in the [setup](#setup).
|
||||
`<path-to-z3>` is the path to the Z3 binary (for example `/bin/z3`) and `<path-to-boogie>` is the
|
||||
path to the boogie binary (for example `~/.dotnet/tools/boogie` when set up with .NET).
|
||||
|
||||
```sh
|
||||
java -jar <path-to-carbon-jar> --z3Exe <path-to-z3> --boogieExe <path-to-boogie> <path-to-viper-file>
|
||||
```
|
||||
10
wiki/ssh.md
Normal file
10
wiki/ssh.md
Normal file
@@ -0,0 +1,10 @@
|
||||
# SSH
|
||||
|
||||
SSH is a network protocoll to securely connect to a computer.
|
||||
|
||||
## Implementations
|
||||
|
||||
There are various implementations of the SSH protocol.
|
||||
|
||||
- [OpenSSH](/wiki/linux/openssh.md) is an SSH implementation for
|
||||
[Linux-based systems](/wiki/linux.md).
|
||||
113
wiki/traefik.md
113
wiki/traefik.md
@@ -7,3 +7,116 @@ a special integration of infrastructure components (e.g. [Docker](./docker.md)).
|
||||
|
||||
The software can be setup via [Docker](/wiki/docker.md) with the
|
||||
[traefik image](./docker/traefik.md).
|
||||
|
||||
## Usage
|
||||
|
||||
This section addresses the usage of Traefik.
|
||||
|
||||
### Redirections for Docker Service
|
||||
|
||||
It is assumed that the service already has a reverse proxy setup as described in the
|
||||
[corresponding section](#reverse-proxies-for-docker-service)
|
||||
For redirections to work they have to be added to the `data/config/dynamic.yml` file.
|
||||
|
||||
For this to work define them inside the `data/config/dynamic.yml` set up in the
|
||||
[Docker image](/wiki/docker/traefik.md) under `middlewares:`.
|
||||
|
||||
Redirections are specified by Regex as shown in the following example.
|
||||
`<redirection-name>` is the name of the redirection and `<regex>` the regular expression to replace
|
||||
while `<replacement>` is the replacement of the regular expression.
|
||||
|
||||
```yml
|
||||
<redirection-name>:
|
||||
redirectregex:
|
||||
permanent: true
|
||||
regex: <regex>
|
||||
replacement: <replacement>
|
||||
```
|
||||
|
||||
The `labels:` section of the [Docker](/wiki/docker.md) services that should use these redirections
|
||||
have to be adapted.
|
||||
The following line needs to be added.
|
||||
`<service-name>` is the name of the service.
|
||||
|
||||
```yml
|
||||
- "traefik.http.routers.<service-name>.middlewares=<redirection-name>@file"
|
||||
```
|
||||
|
||||
Make sure to add the domain that will be redirected to and from the labels aswell.
|
||||
This will look similar like the following.
|
||||
In this case the subdomains `<subdomain-1>` and `<subdomain-2>` under the domain `<domain>` is
|
||||
available, but the exact look can vary since also different domains or more than two addresses can
|
||||
be added.
|
||||
|
||||
```yml
|
||||
- "traefik.http.routers.<service-name>.rule=Host(`<subdomain-1>.<domain>`, `<subdomain-2>.<domain>`)"
|
||||
```
|
||||
|
||||
#### Docker Redirection: Appending a `www.`
|
||||
|
||||
To always append a `www.` to the address the following redirection settings can be used.
|
||||
|
||||
```yml
|
||||
redirect-non-www-to-www:
|
||||
redirectregex:
|
||||
permanent: true
|
||||
regex: "^https?://(?:www\\.)?(.+)"
|
||||
replacement: "https://www.${1}"
|
||||
```
|
||||
|
||||
Additionally follow the setup regarding the service as explained in
|
||||
[the general redirection sectino](#redirections-for-docker-service).
|
||||
|
||||
#### Docker Redirection: Removing a `www.`
|
||||
|
||||
To always remove a `www.` from the address the following redirection settings can be used.
|
||||
|
||||
```yml
|
||||
redirect-www-to-non-www:
|
||||
redirectregex:
|
||||
permanent: true
|
||||
regex: "^https?://www\\.(.+)"
|
||||
replacement: "https://${1}"
|
||||
```
|
||||
|
||||
Additionally follow the setup regarding the service as explained in
|
||||
[the general redirection sectino](#redirections-for-docker-service).
|
||||
|
||||
#### Docker Redirection: Redirect a Domain to Another
|
||||
|
||||
For a simple redirection that replaces a domain with another the following redirection settings can
|
||||
be used.
|
||||
This will redirect the domain `<domain-1>` (for example `www.abc.de`) to domain `<domain-2>` (for
|
||||
example `123.xyz.eu`).
|
||||
|
||||
```yml
|
||||
redirect-<domain-1>-to-<domain-2>:
|
||||
redirectregex:
|
||||
permanent: true
|
||||
regex: "^https://<domain-1>(.*)"
|
||||
replacement: "https://<domain-2>${1}"
|
||||
```
|
||||
|
||||
Additionally follow the setup regarding the service as explained in
|
||||
[the general redirection sectino](#redirections-for-docker-service).
|
||||
|
||||
### Reverse Proxies for Docker Service
|
||||
|
||||
To create a reverse proxy from a docker container add the following lines in the
|
||||
`labels:` section of the `docker-compose.yml` of the service to proxy.
|
||||
|
||||
```yml
|
||||
- "traefik.enable=true"
|
||||
- "traefik.docker.network=proxy"
|
||||
- "traefik.http.routers.<service-name>-secure.entrypoints=websecure"
|
||||
- "traefik.http.routers.<service-name>-secure.rule=Host(`<subdomain>.<domain>`)"
|
||||
- "traefik.http.routers.<service-name>-secure.service=<service-name>"
|
||||
- "traefik.http.services.<service-name>.loadbalancer.server.port=<port>"
|
||||
```
|
||||
|
||||
This configuration automatically redirects http to https.
|
||||
When using this configuration the port specified in the latter lines can be
|
||||
ommitted in the `ports:` section if not used directly.
|
||||
This ensures access only via https and restricts access via ip and port.
|
||||
Change `<service-name>` according to the service you want to publish and `<subdomain>` aswell as
|
||||
`<domain>` to the domain you intent to publish the service to.
|
||||
|
||||
Reference in New Issue
Block a user