microsoft / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
223 stars 80 forks source link

__ser and __deser force datatype to be 8bytes. Cannot send custom packets over network wire #77

Open prpr2770 opened 4 years ago

prpr2770 commented 4 years ago

While using Ivy for networking, based on udp_impl.ivy, I found that using the following definition of a packet:

type packet
interpret packet -> bv[16]
instance pkt_serdes : serdes(packet,bytes, ivy_binary_ser, ivy_binary_deser)
instance net : udp_impl(endpoint_id, packet, ivy_binary_ser, ivy_binary_deser)

Enables, transmitting random messages of 8bytes, with only 2bytes(16bits) that is randomly initialized, while the 6 bytes are initialized to 0x00. The destination thus receives, 8bytes in total, rather than the expected 2bytes.

While trying to debug this issue, I found that the following script for compilation: /ivy/ivy_to_cpp.py provides the following description for __ser:

template <class T> void __ser(ivy_ser &res, const T &inp);
template <>
void __ser<int>(ivy_ser &res, const int &inp) {
    res.set((long long)inp);
}

Which suggests that the packet is interpreted to be a long long. Is there a way, to ensure that the ser and deser, can be modified so that randomized data-packets of length 16bits can be generated, and no extra-padding bytes are sent on the wire?

kenmcmil commented 4 years ago

Yes, it certain makes no sense to use 8 bytes for short bit vectors. Just so I understand your use case, do you need to make Ivy's messages compatible with an existing protocol format or implementation? Or is the issue only the waste of bytes on the wire? Also, are you generating a randomized tester, using 'target=test'?

If you want to be compatible with an existing format, it might be best to send a raw byte stream rather than using Ivy's built-in serializer, which isn't guaranteed to give you any particular format.

prpr2770 commented 4 years ago

I am currently using the randomized tester, by using "target=test". Further, I intend to learn to use Ivy for testing different protocols. I felt there isn't sufficient documentation available to do this, so I've been trying to figure out the functionality from reading the code-scripts.

For now, I'm focusing on just sending messages using UDP, and feel that using Ivy's built-in (de)serializer, is leading to waste of bytes on the wire. I felt I had to use Ivy's built-in serializer for handling this functionality.

If there's another way, to just send raw byte-streams, I would like to learn and use that procedure. I guess, if I were to use Ivy for a protocol, I might have to implement my own serializer/deserializer objects that are bit-precise, compared to the native ivy_serializer.

prpr2770 commented 4 years ago

Further, I noticed that using the randomized tester has some limits. If I define my packet to be the following, it results in the following:

  1. bv[1] - bv[31] : initializes 8 bytes, with upto last 4 bytes being randomized. The leading 4 bytes are always 0x00.
  2. bv[32], it always initializes the packet as 8 bytes of 0x00.
  3. bv[40] : only 1 byte is randomized. The leading 7 bytes are initialized as 0x00. I assume this is because the generating engine, randomly initializes unsigned integers(4bytes long, but not certain about the 31-bits constraint). The serializer/deserializer then enforces the 8-byte length on the data. I would like to generate random messages of any given size (eg bv[40] ) and send them out exactly as the payload of a UDP packet.
kenmcmil commented 4 years ago

It's interesting that there is a threshold between 31 and 32 bits. I'll look into that.

Anyway, you're right that the use of Ivy for testing external software (i.e., not testing Ivy programs) is not documented. There is the example of the QUIC specification in doc/examples/quic, but that is too complicated to get started with. I have simpler examples of testers for IP, UDP and TCP that will probably be more helpful. I will check those in to the repository.

Meanwhile, I'm happy to help with Ivy so you don't have to dig into the Python code :-). Feel free to contact me directly by email and tell me a bit about your application.

kenmcmil commented 4 years ago

Check out the networking branch of Ivy. I have added some examples in the directory doc/examples/networking. In particular, in ip_codec.ivy, udp_codec.ivy and tcp_codec.ivy you can see some examples of custom serializers and deserializers. The main files ip_codec.ivy, udp_codec.ivy and tcp_codec.ivy have some examples of doing raw socket I/O. The .md files describe how to run the examples.

prpr2770 commented 4 years ago

Thank you for sharing this. I have a question, regarding the implementation of tcp_test.ivy

Why is it that, in the implementation of tcp.protocol.transmit, in the scenario where you shall not be queuing the packet, but infact sending it out through the ip-socket, why do you not use tcp_send() to send the packet directly? You seem to be calling two other functions, before handling tcp_send(), which confuses me.

            # Imported call: Q: Does this serve the purpose of logging that this datagram was received. 
            call infer_receive(src,dst,dgram);

            # Why is the protocol receiving a datagram even though the tcp.protocol.send() was a generated event
            # The specification says that all transmitted PROTO-level-datagrams must correspond to 
            # previously sent APP-level-datagram(TCP datagrams)
           # TODO: Is the tcp.protocol.receive() referring to reception of datagram across the PROTOCOL-interface, or is it talking about receiving the datagram internally from the APP-interface? 
            call tcp.protocol.receive(src,dst,dgram,dgram.seq_num_field,dgram.window_field,bfe[0][15](dgram.payload.end));

            # Send the Generated TCP.Datagram over the IP-Socket. 
            call tcp_send(src.addr,dst.addr,dgram);

From tcp_spec.ivy we know that tcp.protocol.transmit() is the main portocol-level-api call. Though, tcp.protocol.receive() has been defined, there's no comments provided about why its needed, and when it shall be invoked. In tcp_test.ivy, we see that tcp.protocol.receive() is invoked whenever, a generated datagram is going to be transmitted over the wire. What does it mean to receive a datagram at the protocol-interface?

prpr2770 commented 4 years ago

Further, in the tcp_test.ivy, we note that the implementation of ip_sock.recv(), which handles the event of obtaining a packet from the OS-RAW-IP socket connected to the protocol-interface of the TCP_Protocol_Spec, DOES NOT call/invoke tcp.protocol.receive().

The received decoded tcp.datagram is parsed, and certain tcp-application-interface-api-calls are invoked {eg. tcp.app.listen(), tcp.app.close(), tcp.app.transmit() }

It surprises me that 'ip_sock.recv()' which is a proxy for a protocol-lnterface event( 'tcp.protocol.recv()' ) is used to trigger an application-lnterface event.

I guess I do not understand how to connect the flow of data internal to the TCP-Protocol-Spec through the application-interface ( tcp.app) and into the protocol-interface(tcp.protocol).

From my understanding of the tcp_test.ivy, we test each interface independent of each other. The tcp.app interface is tested, by connecting it to an OS-TCP-Socket and defining the events corresponding to that. The tcp.protocol interface is tested separately by connecting it to an OS-RAW-IP-Socket and then defining/implementing the events corresponding to it.

kenmcmil commented 4 years ago

I apologize -- it looks like I checked in the wrong files for the TCP tester. I don't that that version even works. I'll try to fix that ASAP.