Search datasets
EASY offers sustainable archiving of research data and access to thousands of datasets.
Source code and data relevant for the paper 'Model Learning and Model Checking of SSH Implementations'
Cite as:
2018 Fiterau-Brostean, P. (Radboud University); Poll, dr. ir. E. (Radboud University); Vaandrager, prof. dr. F.W. (Radboud University); Lenaerts, T.; Ruiter, dr. J.E.J. de (Radboud University); Verleg, P. 10.17026/dans-z6n-dxq6
The dataset contains source code and data relevant for the paper "Model Learning and Model Checking of SSH Implementations".
Paper url: https://dl.acm.org/citation.cfm?id=3092289
PDF url: https://www.cs.ru.nl/E.Poll/papers/learning_ssh.pdf
In this work, we use automata learning with abstraction to infer models of 3 SSH server implementations (BitVise, DropBear, OpenSSH). We then verify properties on these models using the NuSMV model checker. The dataset comprises the software components of our experimental setup apart from the actual implementations, some useful scripts and the learned models and associated experimental logs.
In more concrete terms, the dataset contains:
- the learner (setup) implementation - Java code for the setup built around LearnLib to perform learning over sockets
- the mapper implementation - Python code for the altered Paramiko SSH implementation
- experimental results - learned Mealy Machine models for 3 SSH server implementations (BitVise, OpenSSH, DropBear)
- experimental data - contain additional information not included in experimental results
- various Python scripts
- .dot to .smv converter - Java program for converting Mealy Machine .dot models to .smv model
- .dot beautifying utility - Python program for making models more readable by merging edges between the same nodes
What can be re-used:
- the learner setup (connect to the learner to a different system over sockets)
- Mealy Machine .dot file to NuSMV conversion (convert any .dot to a .smv file suitable for NuSMV, which can be used in model checking)
- Mealy Machine .dot models for 3 SSH implementations (if one wants to do something with the learned models)
- beautifying Python program (if one wants to make complex .dot files more readable)
Also, the dataset is suitable for one who wants to try out/expand learning for SSH.
Paper Abstract: We apply model learning on three SSH implementations to infer state machine models, and then use model checking to verify that these models satisfy basic security properties and conform to the RFCs. Our analysis showed that all tested SSH server models satisfy the stated security properties, but uncovered several violations of the standard.
| Relations | ||
|---|---|---|
|
|