Formal verification of operating system kernelsDenis Efremov
油
The speaker will share his experience of participating in projects on formal verification and analysis of access control modules for Astra Linux SE and Elbrus kernels, as well as verification of the Contiki code (OS for IoT) within the European VESSEDIA program. The speaker will disclose details about the development of formal access control models (Rodin/Event-B) and code specifications (Frama-C/ACSL), the use of static and dynamic analyzers, and the inclusion of formal analysis in the continuous integration cycle (continuous verification). Other types of work that help meet the certification requirements will also be considered.
https://standoff365.com/phdays10/schedule/development/formal-verification-of-operating-system-kernels
Formal verification of operating system kernelsDenis Efremov
油
The speaker will share his experience of participating in projects on formal verification and analysis of access control modules for Astra Linux SE and Elbrus kernels, as well as verification of the Contiki code (OS for IoT) within the European VESSEDIA program. The speaker will disclose details about the development of formal access control models (Rodin/Event-B) and code specifications (Frama-C/ACSL), the use of static and dynamic analyzers, and the inclusion of formal analysis in the continuous integration cycle (continuous verification). Other types of work that help meet the certification requirements will also be considered.
https://standoff365.com/phdays10/schedule/development/formal-verification-of-operating-system-kernels
4. About myself.
Vikentsi Lapa: Software Test Automation Engineer
10 years hands on experience with
Linux:
CDN
Storage systems (DDN), HPC
Coauthour of Linux Essentials
course (this course)
Experienced trainer (Linux, Python,
Scratch)
(MLUG) activist, LVEE speaker
Linux administration course. 2
5. 丶亠仍亠于舒 舒亟亳仂亳
Windows System Adminstrators
IT Engineers, DevOps Engineers
Junior Software Engineers/Software Engineers
Test Engineers, Test Automation Engineers
Students
Linux administration course. 3
6. 丶亠仍亠于舒 舒亟亳仂亳
Windows System Adminstrators
IT Engineers, DevOps Engineers
Junior Software Engineers/Software Engineers
Test Engineers, Test Automation Engineers
Students
丐亠弍仂于舒仆亳 从 舒仆亳从舒仄:
仗 舒弍仂 Linux/Unix 仄亠仆亠 亞仂亟舒 亳仍亳 弍亠亰 仂仗舒
亠仍舒亠仍仆仂: 仂仗 舒弍仂 亳亠仄仂亶 于亳舒仍亳亰舒亳亳
TCP/IP basic knowledge and network configuration skills
Linux administration course. 3
7. 丶亠仍亠于舒 舒亟亳仂亳
Windows System Adminstrators
IT Engineers, DevOps Engineers
Junior Software Engineers/Software Engineers
Test Engineers, Test Automation Engineers
Students
丐亠弍仂于舒仆亳 从 舒仆亳从舒仄:
仗 舒弍仂 Linux/Unix 仄亠仆亠 亞仂亟舒 亳仍亳 弍亠亰 仂仗舒
亠仍舒亠仍仆仂: 仂仗 舒弍仂 亳亠仄仂亶 于亳舒仍亳亰舒亳亳
TCP/IP basic knowledge and network configuration skills
Engagement is essential: answer to questions, do practical
tasks, do homework, ask questions
Linux administration course. 3
17. 亠仆从舒 于仂亰舒舒 亳亠仄 Unix.
舒舒 于亠亳.
1 $ date +%s # show c u r r e n t date in seconds
2 $ echo $ ( ( $ ( date +%s ) /(60*60*24*365) ) ) # show
years
3 $ date help | grep %s
Linux administration course. 8
18. 亠仆从舒 于仂亰舒舒 亳亠仄 Unix.
舒舒 于亠亳.
1 $ date +%s # show c u r r e n t date in seconds
2 $ echo $ ( ( $ ( date +%s ) /(60*60*24*365) ) ) # show
years
3 $ date help | grep %s
Unix systems are characterized by a modular design or Unix
philosophy
simple tools that each perform a limited,
welldefined function
shell scripting and command language to
combine the tools to perform complex
workflows
unified filesystem
Linux administration course. 8
32. VM creation steps
OS type
Virtual Machine Name
Specify disk size, type ( dynamic vs fixed size )
Default network card type is NAT Network
Linux administration course. 19
33. Typing special characters
Special key combinations with the Host key (normally the right
Control key)
Host key to return back to host system from virtual machine
Host key + Del to send Ctrl+Alt+Del (to reboot the guest);
Host key + F1 (or other function keys) to simulate Ctrl+Alt+F1
Linux administration course. 20
39. GNU/Linux Distibution structure
Linux distro is an operation system.
Software Collection
Linux Kernel
Package Management System (optional)
Linux administration course. 25
40. 舒亰仆仂仂弍舒亰亳亠 Linux 亟亳亳弍亳于仂于 亳 仗仂弍仍亠仄舒
于弍仂舒.
丕亞舒亟舒亶从舒. 弌从仂仍从仂 仗仂 于舒亠仄 仄仆亠仆亳 亠于亠 舒从亳于仆
亟亳亳弍亳于仂于?
Linux administration course. 26
44. 亳仄亠 仗仂仗仍仆 Linux 亟亳亳弍亳于仂于.
RedHat
Fedora Core
CentOS
Scientific Linux
Oracle Unbreakable
Linux
Slackware
Gentoo
Arch
OpenSUSE
ALT Linux
Debian
Ubuntu
Mint
Knoppix
BackTrack
Linux administration course. 28
52. Secure Shell (SSH)
Used for:
execute commands
copy files (SFTP, SCP)
forwarding TCP ports and X11 connections
tunneling
SSH uses the clientserver model
The standard TCP port 22
Linux administration course. 34
54. SSH address
Access parameters
IP address: 192.168.10.10
Username: root, val, user
Port: 22 default or any
Full path: root@192.168.10.10:22
Linux administration course. 36
55. 仂仆亳亞舒亳 从仍亳亠仆舒
Linux: .ssh/config
1 Host updateserver
2 Port 8022
3 User k9repo
4 IdentityFile ~ / . ssh / git_rsa
5
6 Host mailtunnel
7 HostName mail . my_isp . net
8 LocalForward 2525: localhost :25
9 GatewayPorts no
10
11 Host elinux
12 User MINSK vshakhov
13 ForwardX11 yes
14 PreferredAuthentications publickey
Windows: PuTTY session
Linux administration course. 37
59. From FAQ How To Ask Questions The Smart Way
Before You Ask try to find an answer
by reading (RTFM): manual, FAQ, archives of the forum, by
searching the Web;
by inspection or experimentation;
by asking a skilled friend;
by reading the source code;
Linux administration course. 39
60. 仂亠仆仆舒 亟仂从仄亠仆舒亳
man 仗仂仄仂 仗仂 于仆亠仆亳仄 从仂仄舒仆亟舒仄
Linux administration course. 40
61. 仂亠仆仆舒 亟仂从仄亠仆舒亳
man 仗仂仄仂 仗仂 于仆亠仆亳仄 从仂仄舒仆亟舒仄
info 舒亳亠仆仆舒 仗仂仄仂 仗仂 仆亠从仂仂仄 从仂仄舒仆亟舒仄
(texinfo format)
Linux administration course. 40
62. 仂亠仆仆舒 亟仂从仄亠仆舒亳
man 仗仂仄仂 仗仂 于仆亠仆亳仄 从仂仄舒仆亟舒仄
info 舒亳亠仆仆舒 仗仂仄仂 仗仂 仆亠从仂仂仄 从仂仄舒仆亟舒仄
(texinfo format)
find /usr/share/doc/ 舒亶仍 亟仂从仄亠仆舒亳亳 仗仂舒于仍磳仄亠
于仄亠亠 仗亳仍仂亢亠仆亳亠仄 (仗亳仄亠 从仂仆亳亞仂于, README)
h, help option 于仂亠仆仆舒 于 仗亳仍仂亢亠仆亳亠 仗舒于从舒
help 于仂亠仆仆舒 仗仂仄仂 仗仂 于仆亠仆仆亳仄 从仂仄舒仆亟舒仄 bash
(舒从亢亠 man bash)
Linux administration course. 40
63. 仆仂于仆仂亠 仂 man
man <command_name>
Example: show uptime manual page
man man
仂亳舒亶亠 man man !
Linux administration course. 41
64. man page navigation
up, down scroll one line
q exit
/pattern search pattern
n next text pattern
N repeat search in back direction
h help
Linux administration course. 42
65. Page structure
NAME
SYNOPSIS
DESCRIPTION
EXAMPLES
SEE ALSO
Linux administration course. 43
67. More than one section of the manual
name(section)
man(1) and man(7), or exit(2) and exit(3)
Example: show manual in section 5 and 1
1 man f passwd # or whatis passwd
2 man 5 passwd ; man 1 passwd ; man wa passwd
Linux administration course. 45
68. 仂亳从 仗仂 舒仆亳舒仄 仗仂仄仂亳
丕仗舒亢仆亠仆亳亠. 仂亳从 舒仆亳 从仍ム亠于仄 仍仂于仂仄.
1 man f passwd # or whatis passwd
2 man k passwd # or apropos passwd
3 whatis l w *
4 man s 3 Kw passwd
Linux administration course. 46