question about branch ralib-0.1_tcp_experimental

[jmc12138]

Hi when I want to build branch 0.1_tcp_experimental,I have faced some issues. The link to jconstraints-z3 is not available,I can only find a version in github(https://github.com/psycopaths/jconstraints-z3). The jar package for jconstraints-z3 compiled by this repository is jconstraints-z3-0.9.1-SNAPSHOT.jar However, the pom.xml file requires jconstraints-z3-0.9.2-SNAPSHOT.jar, and I cannot find version 0.9.2. Perhaps it was the reason why I ultimately passed the compilation, but an error occurred during the testing process:

Execution terminated abnormally: com/microsoft/z3/Z3Exception java.lang.NoClassDefFoundError: com/microsoft/z3/Z3Exception at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59) at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201) at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:225) at de.learnlib.ralib.solver.ConstraintSolverFactory.createZ3ConstraintSolver(ConstraintSolverFactory.java:53) at de.learnlib.ralib.solver.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:39) at de.learnlib.ralib.theory.inequality.InequalityTheoryWithEq.getSolver(InequalityTheoryWithEq.java:100)

my z3 version is 4.4.1 , I have imported com.microsoft.z3.jar into the Maven repository.I followed these two repos((https://github.com/psycopaths/jconstraints-z3 and https://github.com/psycopaths/jconstraints)) to install jconstraints z3 and jconstraints. Can you give me some advices? Thanks

[pfg666]

Hi @jmc12138 ,

Thanks for reporting the issue. There are many small issues in the older branches/versions of RALib which make installing it a pain. In your case, you should update in the pom.xml the dependency for jconstraints-z3 so that the version matches that of the library that you have deployed in your local Maven repository. That should fix your build issue.

[jmc12138]

Thanks for your advice. I followed your advice and failed. but I find I I only want to use the equality theories, so I don't need to study this branch. Can you give me an advice about how to use this tool to study a register automata of a protocol with equality theories? and what branch should I study ? Thanks!

[kostis]

The branch which is actively developed and maintained is main, so I would suggest that you try that one.

May I also suggest that you try to be a bit more specific in what you would like to do and the problems that you are experiencing? For example, the word "study" in the sentence "...how to use this tool to study a register automata of a protocol with equality theories" is quite vague. Similarly, if you experience any (more) problems, the chances that the problems you experience will be fixed increase significantly if you describe what these problems are and how to reproduce them, rather than just mentioning that "I followed your advice and failed", which does not give us any information on what went wrong (and how to possibly help you fix it).

[pfg666]

I concur with @kostis . @jmc12138 , for equality theories, you should just check the main branch. You can use this tool to generate RAs of network protocol implementations. However, in order to do that, you will need to understand what the tool can learn and its limitations, and then design an appropriate test harness, or use an existing one (e.g., dtls-fuzzer for DTLS).

My suggestion is that you actually play with the class-analyzer tool and use it to learn basic class instances mimicking network protocol implementations. This would allow you to get a feel for the tool, and should not take much of your time. Afterwards, you can take an existing protocol, build infrastructure for learning based on RALib and generate models for implementations. This is something that will require weeks/months to do, since the infrastructure is currently not there and/or needs updating. If you are interested in this, let me know.

[jmc12138]

Thanks for your advice@kostis,@pfg666 . I am a graduate student. I'm interested in study a register automaton for IPsec and describe its connection establishment process using equality theories. Currently, I have modified the class-analyzer into a socket-analyzer to study automata based on socket interactions. I'm interested in Contribute to this project. My aim is to add an test harness to study Establishment behavior of cryptographic protocols like TLS and IPsec. but I'm a beginner in Java. If you don't mind, can I contribute to this project？@pfg666 Thanks

[pfg666]

Hello again!

Doing RA learning of IPsec stacks seems interesting. Note that RALib is a generic learning library. So we would like to avoid adding to it protocol-specific content. I hence suggest you create a fork of RALib and tweak it for IPsec, e.g., in a similar to how RALib was tweaked for TCP. If there are things that you need that you feel should be in the main RALib repo, post an issue/create a PR.

Due to current circumstances I cannot provide much technical guidance in this effort, so you will need to do the digging yourself.
Here is how I would go about implementing it:

1. build an IPsec server adapter, this thing communicates with the learner (RALib) over a socket connection, it receives from the learner for packet/command strings, converts them into actual packets and sends them to an IPsec implementation, receives the response packet, extracts the packet string, and sends it back to the learner. A packet string is an abstract representation of a packet (e.g., CLIENT_HELLO(epoch:0) could be the abstract representation of a ClientHello message with epoch field set to 0). The server adapter can additionally reset/restart the IPsec implementation.
2. add into RALib a tool for communicating with the server adapter over sockets, such a tool already exists in the succ-stable branch (named socket-analyzer), which is a branch we built by removing all TCP-specific functionality. However, the succ-stable branch has not been updated, it's probably easier to build the tool from scratch, copy-pasting functionality from the succ-stable branch whenever appropriate
3. create config files with the appropriate theories for IPsec, and start doing experiments.

What I like with this approach is that you can test/use the IPsec server adapter independently of the learner. You can, for example, send commands to it over something like telnet and ensure it responds correctly. This also allows for the adapter to be implemented in a language other than Java (Python springs to mind). Once you are confident that the IPsec server adapter works (you can complete handshakes over telnet), then you can start work on the learner component.

P.S., You might want to check this publication, they do regular learning of IPsec. A good place to start is to replicate their work. See if you can use their tools, instead of building everything from scratch.

[jmc12138]

Thanks for your advice ,this paper is the work of my senior fellow. It's so wonderful how fate has brought us together here！

[pfg666]

I suggest you contact them. Having a public and (hopefully) well-maintained server adapter for IPsec would be very useful.