Commit a7a9048f by Erik Poll

### fixed some times & condensed

parent 7145da0a
 ... ... @@ -9,10 +9,10 @@ Abstraction was provided by a {\dmapper} component placed between the {\dlearner} and the {\dsut}. The {\dmapper} was constructed from an existing SSH implementation. The input alphabet of the {\dmapper} explored key exchange, setting up a secure connection, several authentication methods and opening and closing channels over which the authentication methods, and opening and closing channels over which the terminal service could be requested. We used two input alphabets, a full version for OpenSSH, and a restricted version for the other implementations. The restricted alphabet was still sufficient to full version for OpenSSH, and a restricted version for Bitvise and DropBear. The restricted alphabet was still sufficient to explore most aforementioned behavior. We encountered several challenges. Firstly, building a {\dmapper} presented a considerable technical challenge, as it required re-structuring of an actual ... ...
 ... ... @@ -86,7 +86,7 @@ also used model checkers \cite{TCP2016,Chalupar2014Automated}. Instead of using active learning as we do, it is also possible to use passive learning to obtain protocol state machines \cite{Wang2011Inferring}. Here network traffic is observed, and not actively generated. This can then also provide a probabilistic actively generated. This can then provide a probabilistic characterization of normal network traffic, but it cannot uncover implementation flaws that occur in strange message flows, which is our goal. ... ...
 ... ... @@ -21,8 +21,9 @@ We have adapted the setting of timing parameters to each implementation. \end{figure*} OpenSSH was learned using a full alphabet, whereas DropBear and BitVise were learned using a restricted alphabet (as defined in Subsection~\ref{subsec:alphabet}). The main reason for using a restricted alphabet reduce learning times. Based on the model learned for OpenSSH (the first implementation analyzed) and the specification, we excluded inputs that seemed unlikely to produce state change (like \textsc{debug} or \textsc{unimpl}). We also excluded inputs that proved costly time-wise (like \textsc{disconnect}), yet were not were not needed to visit all states in our happy flow. We excluded, for example, the user/password based authentication inputs (\textsc{ua\_pw\_ok} and The reason for using a restricted alphabet was to reduce learning times. Based on the model learned for OpenSSH (the first implementation analyzed) and the specification, we excluded inputs that seemed unlikely to produce state change (such as \textsc{debug} or \textsc{unimpl}). We also excluded inputs that proved costly time-wise (such as \textsc{disconnect}) but were not were not needed to visit all states in the happy flow. We excluded, for example, the user/password based authentication inputs (\textsc{ua\_pw\_ok} and \textsc{ua\_pw\_nok}) as they would take the system 2-3 seconds to respond to. By contrast, public key authentication resulted in quick responses. %The \textsc{disconnect} input presented similar ... ... @@ -45,8 +46,8 @@ can be set to higher values. We executed a random test suite with {\dk} of 4 com %To that end, we built a java adapter that would automatically run the model checker on the hypothesis, and transform any counterexamples into tests. This proved essential in learning DropBear, as the last counterexample was generated by the model checker. Table~\ref{tab:experiments} describes the exact versions of the systems analyzed together with statistics on learning and testing, namely: (1) the number of states in the learned model, (2) the number of hypotheses built during the learning process and (3) the total number of learning and test queries run. For test queries, we only consider those run on the last hypothesis. All learned models plus the specifications checked can be found at \url{https://gitlab.science.ru.nl/pfiteraubrostean/Learning-SSH-Paper/tree/master/models}. The statistics Table~\ref{tab:experiments} describes the exact versions of the systems analyzed together with statistics on learning and testing: (1) the number of states in the learned model, (2) the number of hypotheses built during the learning process and (3) the total number of learning and test queries run. For test queries, we only consider those run on the last hypothesis. All learned models and the properties checked are at \url{https://gitlab.science.ru.nl/pfiteraubrostean/Learning-SSH-Paper/tree/master/models}. The statistics give a glimpse into the issue of scalability. Assuming each input took 0.5 seconds to process, and an average query length of 10, to perform 40000 queries would have taken roughly 55 hours. This is consistent with the time experiments took, which span several days. The long duration compelled us to resort to restricted alphabets, which lead to reduction in the number of queries needed. Our work could have benefited from parallel execution. %BitVise: MemQ: 24996 TestQ: 58423 %Dropbear: MemQ: 3561 TestQ: 30629 ... ...
{"extraction_info": {"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8393713235855103, "perplexity": 2546.0449483867014}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2021-43/segments/1634323588526.57/warc/CC-MAIN-20211028193601-20211028223601-00677.warc.gz"}