RecordFlux: Facilitating the Verification of Communication Protocols
Reiher, Tobias
Many security problems have been discovered in communication protocols in the past, examples are: BlueBorne, a set of security vulnerabilities in the Bluetooth implementation which affect millions of devices Heartbleed, a security bug in the OpenSSL library that lead to exposure of sensitive data CVE-2018-10933, a critical bug in libssh which allows successful authentication without any credentials Still today many critical issues remain in protocol implementations, as their root causes have not been addressed. Two classes of faults dominate: runtime errors like buffer overflows, and logic errors in protocol state machines. The main reasons for runtime errors is the use of unsafe programming languages. Better alternatives with formal guarantees like Rust, SPARK or Frama-C exist, but re-implementing complex protocols means a lot of effort. Logic errors are caused by the complexity of protocols and imprecise specifications in natural language. RecordFlux is a framework for the secure implementation of communication protocols. From a formal protocol specification written in a domain-specific language the tools generate SPARK code, for which the absence of runtime errors can be proven automatically. In the future RecordFlux will also allow the specification of dynamic protocol semantics and support formal correctness proofs for protocol state machines. In this talk we give an overview of the current state and speak about an upcoming project that uses RecordFlux for a complex real-world application, the compartmentalized implementation of TLS 1.3 for component-based operating systems.
 So, hello everyone. Please welcome Tobias Leihar on Record Flux, facilitating the verification of communication protocols. Thank you. Thank you for coming. I'm here with a network with an overview about the problems we have seen in the communication protocol implementations. And then I will talk about our solution to these problems. And at the end give a short outlook on what we are planning to do with Record Flux in the future. So in the past we have seen multiple security vulnerabilities in communication protocols. Here are just three examples. There we have BlueBorne that was a set of vulnerabilities which was found in the implementation of Bluetooth. And this vulnerability affected millions of devices. And an attacker was able to take over the full control of the device and also to write a mailbox which spreads wirelessly from device to device. Also very famously is the HardBeat vulnerability, a bug which was found in the open as an implementation of the TLS HardBeat extension. And there it was possible to extract sensitive data out of another TLS endpoint. Another interesting bug was found last year in the implementation of LibSSH. There it was possible to circumvent authentication process by just sending one message at exact time. So without knowing a password or a key or something like that, you can just get access to the SSH server. What we can see from these vulnerabilities is that at all software layers we have found such vulnerabilities even from very low level implementations like Bluetooth or TLS to application layer applications like SSH. But what are the cause for these problems? So when we look at communication protocols, they are usually very complex. And implementing complex protocols is very time consuming and also error prone. Also the specifications play an important role. Such specifications are usually only available in English pros and so it's easily misunderstood by a developer or it's easy to misinterpret or forget to implement some detail. Also maybe look at the specifications, they are not formally specified. So if you had those formal specifications, it would be able to verify that the implementation we did is correct at the end. But as such formal specifications does not exist, it's not possible yet. We could see communication protocols consist of multiple parts. We have messages which are described by formats. We have the protocols in Mantik which is described usually by a state machine which tells us at which time which message is expected. And for security protocols we also have something like security properties which define if a message or data in a message has properties like integrity or confidentiality. To tackle the vulnerabilities we have seen in communication protocols, we have to tackle each part. But as foundation we need to ensure that no one time errors exist. So we have to make sure that no buffer overflows, integer overflows or something like that are in implementation. By using verification techniques we could do that by program verification. Then when we have this foundation we can look at the messages to ensure that the message formats are correct. We could use functional correctness proofs and with this proofs we can ensure that vulnerabilities like we have seen in Bluebourne or on Heartbleed that these vulnerabilities are prevented. Then at the next level we have also to ensure the protocols in Mantik of course. There are different techniques possible. We could use temporal logic or model checking and when we have also dis-insured then we can prevent errors like seen in SSH. And further step further then we also have to ensure the security properties of security protocols. And therefore we could think of using security protocol proofs to ensure also that implementation fulfills the properties which we want to fulfill it. But let's start at the foundation. Let's look at the absence of runtime errors. So solve this problem. We are using Spark. Spark is a programming language and a verification tool set. And it's especially designed for error avoidance. So this is the reason that Spark contains features like a strong type system and formal contracts. And it's especially also used in this area then. Also the application tool set is able to do a flexible depth of application. So you can prove data and control flows. You can prove dependency contracts. You can even prove that there are no runtime errors exist. Or you can even do more and prove the function correctness of the code. Because of the features it is used in critical projects. So you can think of areas with high safety requirements like aerospace or areas with high security requirements like government or defense area. As it's a compiled language it can also be used for system level programming. And so it's also used in implementation of microcodes. If you're interested in Spark you can find more details on the website of Adaco which still develops these tools. So see the power of Spark is a simple example. We have here a simple z function which calculates absolute value of an integer x. This function mainly consists of an if statement where it is checked that x is greater than zero. If this is the case then x is returned and otherwise the negative value of x is returned. Maybe someone sees already an error there. For the most case it works fine. So we can put some numbers in there and we get the correct number back. But in one case we get not the correct value back. What's the reason for that? The representation of the integer uses the truth complement. And this means that not for all negative numbers we have also a positive counterpart part. So in this case this is the lowest negative number which is possible to see in the end. And if you want to, if you try to negate this value then we get an integer overflow and get at the end back in negative value. If we now implement this function in the same way with Spark we can use the Spark tools to verify if there are any errors exist in the code. The nice thing about this Spark tools is that you don't have to run the code or even compile it. You can just run it on the source code and it will check if there are any errors existing. So in this case at line 6 you see that Spark tools found an error. They also tell us what error is. So they found an overflow check, fail, and also give us a hint what the example is when the event happens. So here it tells us that when x equals integer first then we have an overflow fail. It also gives us a hint what we can do to prevent this error. We could add a precondition here. So this is the function body but the precondition is added to the specification. And you see if we now add a precondition which states that x must not be integer first and then run the Spark tools again. On this function the Spark tools will see that this error will not occur anymore. So you see the Spark tools are able to prevent one-time errors but we can even do more. And that is what we are doing with FACOT Flux. But what is the goal of FACOT Flux? We want to be able to dissect, generate, and verify communication protocols. At the current stage we are focusing on the specification and the parsing of messages but in the future we also want to do more. So FACOT Flux currently consists of a specification language which is able to describe protocol messages. We implemented a parser which is able to parse such a specification and creates an intermediate representation out of it which is then used by a generator to generate Spark code of it. And the Spark code can then be used to verify protocol messages and also parse them. Here is the example. So our specification language is inspired by ETA but we adapted it to fit our purpose. So here in this example we describe a simple message. It's a TS-HARPID message which consists of four fields. So we have a message type field, we have a payload link field, a payload field, and a padding field. The first two fields are fixed in their size and the two fields at the end are variable. We represent such a message by using a message type which is similar to the direct or the swag type in Z. It looks like that. We have just listed all field names and also the type of the field. Then we also have to define of course the type of the field. And then we could now think what would be an adequate type for the message type field at first. So the message type field has a size of one byte so we could think we use just an integer in size of one byte. But that's not really the best use case. So when we look in the specification we will see that only two possible values are valid for message type. And that's one as a HARPID request and two as a HARPID response. So we are using here an enamiration type where we only specify these two possible values. And now if we see a message which does not contain one of these two values we already see that this is not a valid HARPID message. The same I'll be doing with the payload length field. There we also specify restricted integer which only consists of the values from 0 to 2 to the power of 14 minus 20 because that's the size of the payload field. So for the payload and padding field we use here an composite type which is a built-in type which is called payload type. And this just represents a variable size byte array. To make our specification also modular we have to put all types in the name package which is here called TSHARPID. When we look now at the specification it's not really complete as we didn't specify the length constrained for the whole message. And the length constrained of the padding field. So we need to do more. Also what is missing is the relation between the length feed and the payload feed. And this relation is especially important. As we have seen in HARPID that this relation was not respected and so it was possible to send in HARPID request with a high value for the payload length but only in small payload. And then the receiver of such a request has to copy the payload back but did not check if it really fits to the payload that she gets. And so you just read all the data according to the payload length and so read also more data, not also only the message. And this data could be potentially confidential like keys or something like that. So this relation is really important. Here is the full specification of the message. Highlighted are the length expressions in green and the message constraints in orange. Internally we use a representation of our messages in a graph like form. Where each field of the message is represented by a node and the nodes are connected by edges to specify the order of the fields. We can also add further information to edges so we can add length expressions like it is done here between the payload length field and the payload field. And there we specify that the length of the payload field is the value of the payload length field multiplied with 8. Here because the payload length is given in bytes but the length in our specification is given in bit length. We also specify in the same way the length of the padding field by just seeing the padding field as the rest of the message. And we also add restrictions for the message length here. The message length has to be smaller than its value and the padding length has to be at least 16 bytes. This is a rather simple example. We could see the full advantage of our model for more complex protocol messages. So we can also represent optional fields by adding an edge which skips some nodes. We can also represent by a condition that we have some fields which are optionally inserted or also fields which have a different meaning depending on the type. So you could think of ethernet. There you have either type field which is depending on its value interpreted as a length field or as a type field. Here we excerpt of the code which we generate. So all functions which we generate for our message use as input in plain byte array which is then used to do further stuff on it. We generate verification code and access code. The verification code for each method checks that the message is valid until to this point. And if we check that we can then access the value and select the value by the access function. So for example for the message type field we have the message type function and a get message type function. And by using preconditions here we ensure that we first have to check the message type field if it's really a message type and only if it is the case then we can access it. For convenience we have also a function which is quote is valid which checks all fields one by one. And if there's a valid path from the start node to the target node then this function returns to and we can then just access all functions on their own without checking again and again. It's also possible to represent the relation between a payload field and another protocol layer. We can see that payload field under some conditions contain another protocol message and this is also checked at the code level. So therefore we have this is contained predicate here which is a precondition for all functions like you can see. And so we ensure that if a developer or use of the code and reuse it to divide buffer. You can only use a buffer which is labeled correctly as a message in this case like a heartbeat message and so ensure that he does not use the wrong buffer. Let's have a look how we can use the generated code. Here we have a small function where we get the byte array from external source by this virtual read function here. We have to label the buffer here like I already said because we get it from external source is not labeled yet. We have to ensure that it is a buffer which potentially contains a heartbeat message. And only after we have to that done that we can access them the fields of the message. As we already specified the relation between the length and the payload field. The user does not have to access the link field anymore. We have to concentrate on the fields which are really relevant for him which means here the type field and the payload field. But there's still an error here in this code. If you run the Spark tools they will tell us that we cannot just call them like it is here. They tell us that a precondition might fail. What is the reason for that? We did not check the validity. So we have to first check if the field is valid. What we do here with an isValid function and by adding this if statement with a valid function and only accessing the fields. If we get a positive result back we ensure that we only access valid messages. We could alternatively also check each field by one by one and also find out where the error in the message occurred. Looking back what we have achieved so far by using Spark we ensure that no runtime errors exist in our implementation. We have built a tracker flux to also correctly identify if a message is valid. And if this is the case we can also access the fields of the message. In the future we also want to represent the protocol semantics in Wecker Flux and also ensure this part of the protocol. And further down the road we also want to use security protocol proofs to ensure that for security protocols also the security properties are fulfilled in the code which we generate. We will use Wecker Flux for a project which is called QTLS. QTLS is a component based insurance implementation of TLS 1.3. So this project just started this year and is partially funded by the European Union and the state of Saxony. And the essential part of this project is that we want to split the implementation of TLS in critical and non-critical parts. And especially for the critical parts we want to use Spark and Wecker Flux to make sure that they are really correct. As a base platform we want to use the G-Node OS framework but potentially also others will be supported. We see multiple challenges in this project so we have to find out how do we do the separation and get at the end sensible implementation of TLS. How can we prove that implementation at the end is secure? And of course we also want to achieve good performance and also see that implementation has no side channels in it. As the project just started this year there is not much done yet but there is already a repository on GitHub and the source code will also be available in the future. Coming to the conclusion, we have already created a specification language which is powerful enough to specify real-world binary protocols. We already specified ethernet including Vlientax, IPv4 and UDP and are currently working on specifying TLS 1.3. We are able to generate Spark code based on the specification and prove for this generated code that no one-time offers exist and that messages correctly identified as correct or incorrect. Backup flux is still in development so we have found some minor bugs by specifying TLS 1.3 which I am working on currently but the bigger thing which we also want to do is adding the method generation. Currently we can only pass messages but we want also to be able to generate messages based on our specification. After that we also want to be able to specify more protocols. We already looked into USB and there we saw that there are also some features are missing. Currently we are focusing on the TLV method scheme that means that we steadily compute where the field starts and how long the fields are based on other fields and based on length fields. But in some cases this is not possible. So there are protocols where you have to do this at a time time and find out where the next field starts. You can think of areas which contain various sized elements and you have to first pass these elements before you know where the second area starts. But that's something that we also want to support in the future. So at the end also the code of packet flux is available online so if you want to have a look at it or look at the documentation you find it on GitHub. So thank you. Thank you. So are there any questions? Hi. How do you handle hardware specificities like out of Rx execution or reshuffling of instructions? Do you model hardware at all? No, we are not at that level. We are modeling just the messages and generating code should then pass these messages. So you're not working on side channel things? That's something that we want to do in the future also looking at the side channels but that's not currently done yet. Anything else? So thank you.
 So, hello everyone.  Please welcome Tobias Leihar on Record Flux, facilitating the verification of communication  protocols.  Thank you.  Thank you for coming.  I'm here with a network with an overview about the problems we have seen in the communication  protocol implementations.  And then I will talk about our solution to these problems.  And at the end give a short outlook on what we are planning to do with Record Flux in the future.  So in the past we have seen multiple security vulnerabilities in communication protocols.  Here are just three examples.  There we have BlueBorne that was a set of vulnerabilities which was found in the implementation of Bluetooth.  And this vulnerability affected millions of devices.  And an attacker was able to take over the full control of the device and also to write a mailbox  which spreads wirelessly from device to device.  Also very famously is the HardBeat vulnerability, a bug which was found in the open as an implementation of the TLS HardBeat extension.  And there it was possible to extract sensitive data out of another TLS endpoint.  Another interesting bug was found last year in the implementation of LibSSH.  There it was possible to circumvent authentication process by just sending one message at exact time.  So without knowing a password or a key or something like that, you can just get access to the SSH server.  What we can see from these vulnerabilities is that at all software layers we have found such vulnerabilities  even from very low level implementations like Bluetooth or TLS to application layer applications like SSH.  But what are the cause for these problems?  So when we look at communication protocols, they are usually very complex.  And implementing complex protocols is very time consuming and also error prone.  Also the specifications play an important role.  Such specifications are usually only available in English pros and so it's easily misunderstood by a developer  or it's easy to misinterpret or forget to implement some detail.  Also maybe look at the specifications, they are not formally specified.  So if you had those formal specifications, it would be able to verify that the implementation we did is correct at the end.  But as such formal specifications does not exist, it's not possible yet.  We could see communication protocols consist of multiple parts.  We have messages which are described by formats.  We have the protocols in Mantik which is described usually by a state machine which tells us at which time which message is expected.  And for security protocols we also have something like security properties which define if a message or data in a message  has properties like integrity or confidentiality.  To tackle the vulnerabilities we have seen in communication protocols, we have to tackle each part.  But as foundation we need to ensure that no one time errors exist.  So we have to make sure that no buffer overflows, integer overflows or something like that are in implementation.  By using verification techniques we could do that by program verification.  Then when we have this foundation we can look at the messages to ensure that the message formats are correct.  We could use functional correctness proofs and with this proofs we can ensure that vulnerabilities like we have seen in Bluebourne or on Heartbleed  that these vulnerabilities are prevented.  Then at the next level we have also to ensure the protocols in Mantik of course.  There are different techniques possible.  We could use temporal logic or model checking and when we have also dis-insured then we can prevent errors like seen in SSH.  And further step further then we also have to ensure the security properties of security protocols.  And therefore we could think of using security protocol proofs to ensure also that implementation fulfills the properties which we want to fulfill it.  But let's start at the foundation.  Let's look at the absence of runtime errors.  So solve this problem.  We are using Spark.  Spark is a programming language and a verification tool set.  And it's especially designed for error avoidance.  So this is the reason that Spark contains features like a strong type system and formal contracts.  And it's especially also used in this area then.  Also the application tool set is able to do a flexible depth of application.  So you can prove data and control flows.  You can prove dependency contracts.  You can even prove that there are no runtime errors exist.  Or you can even do more and prove the function correctness of the code.  Because of the features it is used in critical projects.  So you can think of areas with high safety requirements like aerospace or areas with high security requirements like government or defense area.  As it's a compiled language it can also be used for system level programming.  And so it's also used in implementation of microcodes.  If you're interested in Spark you can find more details on the website of Adaco which still develops these tools.  So see the power of Spark is a simple example.  We have here a simple z function which calculates absolute value of an integer x.  This function mainly consists of an if statement where it is checked that x is greater than zero.  If this is the case then x is returned and otherwise the negative value of x is returned.  Maybe someone sees already an error there.  For the most case it works fine. So we can put some numbers in there and we get the correct number back.  But in one case we get not the correct value back.  What's the reason for that?  The representation of the integer uses the truth complement.  And this means that not for all negative numbers we have also a positive counterpart part.  So in this case this is the lowest negative number which is possible to see in the end.  And if you want to, if you try to negate this value then we get an integer overflow and get at the end back in negative value.  If we now implement this function in the same way with Spark we can use the Spark tools to verify if there are any errors exist in the code.  The nice thing about this Spark tools is that you don't have to run the code or even compile it.  You can just run it on the source code and it will check if there are any errors existing.  So in this case at line 6 you see that Spark tools found an error.  They also tell us what error is.  So they found an overflow check, fail, and also give us a hint what the example is when the event happens.  So here it tells us that when x equals integer first then we have an overflow fail.  It also gives us a hint what we can do to prevent this error.  We could add a precondition here.  So this is the function body but the precondition is added to the specification.  And you see if we now add a precondition which states that x must not be integer first and then run the Spark tools again.  On this function the Spark tools will see that this error will not occur anymore.  So you see the Spark tools are able to prevent one-time errors but we can even do more.  And that is what we are doing with FACOT Flux.  But what is the goal of FACOT Flux?  We want to be able to dissect, generate, and verify communication protocols.  At the current stage we are focusing on the specification and the parsing of messages but in the future we also want to do more.  So FACOT Flux currently consists of a specification language which is able to describe protocol messages.  We implemented a parser which is able to parse such a specification and creates an intermediate representation out of it which is then used by a generator to generate Spark code of it.  And the Spark code can then be used to verify protocol messages and also parse them.  Here is the example.  So our specification language is inspired by ETA but we adapted it to fit our purpose.  So here in this example we describe a simple message.  It's a TS-HARPID message which consists of four fields.  So we have a message type field, we have a payload link field, a payload field, and a padding field.  The first two fields are fixed in their size and the two fields at the end are variable.  We represent such a message by using a message type which is similar to the direct or the swag type in Z.  It looks like that.  We have just listed all field names and also the type of the field.  Then we also have to define of course the type of the field.  And then we could now think what would be an adequate type for the message type field at first.  So the message type field has a size of one byte so we could think we use just an integer in size of one byte.  But that's not really the best use case.  So when we look in the specification we will see that only two possible values are valid for message type.  And that's one as a HARPID request and two as a HARPID response.  So we are using here an enamiration type where we only specify these two possible values.  And now if we see a message which does not contain one of these two values we already see that this is not a valid HARPID message.  The same I'll be doing with the payload length field.  There we also specify restricted integer which only consists of the values from 0 to 2 to the power of 14 minus 20  because that's the size of the payload field.  So for the payload and padding field we use here an composite type which is a built-in type which is called payload type.  And this just represents a variable size byte array.  To make our specification also modular we have to put all types in the name package which is here called TSHARPID.  When we look now at the specification it's not really complete as we didn't specify the length constrained for the whole message.  And the length constrained of the padding field.  So we need to do more.  Also what is missing is the relation between the length feed and the payload feed.  And this relation is especially important.  As we have seen in HARPID that this relation was not respected and so it was possible to send in HARPID request with a high value for the payload length  but only in small payload.  And then the receiver of such a request has to copy the payload back but did not check if it really fits to the payload that she gets.  And so you just read all the data according to the payload length and so read also more data, not also only the message.  And this data could be potentially confidential like keys or something like that.  So this relation is really important.  Here is the full specification of the message.  Highlighted are the length expressions in green and the message constraints in orange.  Internally we use a representation of our messages in a graph like form.  Where each field of the message is represented by a node and the nodes are connected by edges to specify the order of the fields.  We can also add further information to edges so we can add length expressions like it is done here between the payload length field and the payload field.  And there we specify that the length of the payload field is the value of the payload length field multiplied with 8.  Here because the payload length is given in bytes but the length in our specification is given in bit length.  We also specify in the same way the length of the padding field by just seeing the padding field as the rest of the message.  And we also add restrictions for the message length here.  The message length has to be smaller than its value and the padding length has to be at least 16 bytes.  This is a rather simple example.  We could see the full advantage of our model for more complex protocol messages.  So we can also represent optional fields by adding an edge which skips some nodes.  We can also represent by a condition that we have some fields which are optionally inserted or also fields which have a different meaning depending on the type.  So you could think of ethernet.  There you have either type field which is depending on its value interpreted as a length field or as a type field.  Here we excerpt of the code which we generate.  So all functions which we generate for our message use as input in plain byte array which is then used to do further stuff on it.  We generate verification code and access code.  The verification code for each method checks that the message is valid until to this point.  And if we check that we can then access the value and select the value by the access function.  So for example for the message type field we have the message type function and a get message type function.  And by using preconditions here we ensure that we first have to check the message type field if it's really a message type and only if it is the case then we can access it.  For convenience we have also a function which is quote is valid which checks all fields one by one.  And if there's a valid path from the start node to the target node then this function returns to and we can then just access all functions on their own without checking again and again.  It's also possible to represent the relation between a payload field and another protocol layer.  We can see that payload field under some conditions contain another protocol message and this is also checked at the code level.  So therefore we have this is contained predicate here which is a precondition for all functions like you can see.  And so we ensure that if a developer or use of the code and reuse it to divide buffer.  You can only use a buffer which is labeled correctly as a message in this case like a heartbeat message and so ensure that he does not use the wrong buffer.  Let's have a look how we can use the generated code.  Here we have a small function where we get the byte array from external source by this virtual read function here.  We have to label the buffer here like I already said because we get it from external source is not labeled yet.  We have to ensure that it is a buffer which potentially contains a heartbeat message.  And only after we have to that done that we can access them the fields of the message.  As we already specified the relation between the length and the payload field.  The user does not have to access the link field anymore.  We have to concentrate on the fields which are really relevant for him which means here the type field and the payload field.  But there's still an error here in this code.  If you run the Spark tools they will tell us that we cannot just call them like it is here.  They tell us that a precondition might fail.  What is the reason for that?  We did not check the validity.  So we have to first check if the field is valid.  What we do here with an isValid function and by adding this if statement with a valid function and only accessing the fields.  If we get a positive result back we ensure that we only access valid messages.  We could alternatively also check each field by one by one and also find out where the error in the message occurred.  Looking back what we have achieved so far by using Spark we ensure that no runtime errors exist in our implementation.  We have built a tracker flux to also correctly identify if a message is valid.  And if this is the case we can also access the fields of the message.  In the future we also want to represent the protocol semantics in Wecker Flux and also ensure this part of the protocol.  And further down the road we also want to use security protocol proofs to ensure that for security protocols also the security properties are fulfilled in the code which we generate.  We will use Wecker Flux for a project which is called QTLS.  QTLS is a component based insurance implementation of TLS 1.3.  So this project just started this year and is partially funded by the European Union and the state of Saxony.  And the essential part of this project is that we want to split the implementation of TLS in critical and non-critical parts.  And especially for the critical parts we want to use Spark and Wecker Flux to make sure that they are really correct.  As a base platform we want to use the G-Node OS framework but potentially also others will be supported.  We see multiple challenges in this project so we have to find out how do we do the separation and get at the end sensible implementation of TLS.  How can we prove that implementation at the end is secure?  And of course we also want to achieve good performance and also see that implementation has no side channels in it.  As the project just started this year there is not much done yet but there is already a repository on GitHub and the source code will also be available in the future.  Coming to the conclusion, we have already created a specification language which is powerful enough to specify real-world binary protocols.  We already specified ethernet including Vlientax, IPv4 and UDP and are currently working on specifying TLS 1.3.  We are able to generate Spark code based on the specification and prove for this generated code that no one-time offers exist and that messages correctly identified as correct or incorrect.  Backup flux is still in development so we have found some minor bugs by specifying TLS 1.3 which I am working on currently but the bigger thing which we also want to do is adding the method generation.  Currently we can only pass messages but we want also to be able to generate messages based on our specification.  After that we also want to be able to specify more protocols. We already looked into USB and there we saw that there are also some features are missing.  Currently we are focusing on the TLV method scheme that means that we steadily compute where the field starts and how long the fields are based on other fields and based on length fields.  But in some cases this is not possible. So there are protocols where you have to do this at a time time and find out where the next field starts.  You can think of areas which contain various sized elements and you have to first pass these elements before you know where the second area starts.  But that's something that we also want to support in the future.  So at the end also the code of packet flux is available online so if you want to have a look at it or look at the documentation you find it on GitHub.  So thank you.  Thank you.  So are there any questions?  Hi. How do you handle hardware specificities like out of Rx execution or reshuffling of instructions? Do you model hardware at all?  No, we are not at that level. We are modeling just the messages and generating code should then pass these messages.  So you're not working on side channel things?  That's something that we want to do in the future also looking at the side channels but that's not currently done yet.  Anything else?  So thank you.
RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_0_47.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_48_107.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_108_155.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_156_395.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_396_443.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_444_1067.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_1068_4439.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_4440_4691.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_4692_4739.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_4740_4835.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_4836_5195.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_5196_5243.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_5244_7475.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_7476_9335.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_9336_9995.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_9996_10163.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_10164_10979.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_10980_12431.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_12432_12851.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_12852_14135.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_14136_15143.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_15144_19115.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_19116_22139.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_22140_25223.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_25224_26639.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_26640_27383.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_27384_28451.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_28452_30335.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_30336_35327.png RecordFlux__Facilitating_the_Verification_of_Communication_Protocols_017ksJ_0uYE_35328_35441.png
So, hello everyone. Please welcome Tobias Leihar on Record Flux, facilitating the verification of communication protocols. Thank you. Thank you for coming. I'm here with a network with an overview about the problems we have seen in the communication protocol implementations. And then I will talk about our solution to these problems. And at the end give a short outlook on what we are planning to do with Record Flux in the future. So in the past we have seen multiple security vulnerabilities in communication protocols. Here are just three examples. There we have BlueBorne that was a set of vulnerabilities which was found in the implementation of Bluetooth. And this vulnerability affected millions of devices. And an attacker was able to take over the full control of the device and also to write a mailbox which spreads wirelessly from device to device. Also very famously is the HardBeat vulnerability, a bug which was found in the open as an implementation of the TLS HardBeat extension. And there it was possible to extract sensitive data out of another TLS endpoint. Another interesting bug was found last year in the implementation of LibSSH. There it was possible to circumvent authentication process by just sending one message at exact time. So without knowing a password or a key or something like that, you can just get access to the SSH server. What we can see from these vulnerabilities is that at all software layers we have found such vulnerabilities even from very low level implementations like Bluetooth or TLS to application layer applications like SSH. But what are the cause for these problems? So when we look at communication protocols, they are usually very complex. And implementing complex protocols is very time consuming and also error prone. Also the specifications play an important role. Such specifications are usually only available in English pros and so it's easily misunderstood by a developer or it's easy to misinterpret or forget to implement some detail. Also maybe look at the specifications, they are not formally specified. So if you had those formal specifications, it would be able to verify that the implementation we did is correct at the end. But as such formal specifications does not exist, it's not possible yet. We could see communication protocols consist of multiple parts. We have messages which are described by formats. We have the protocols in Mantik which is described usually by a state machine which tells us at which time which message is expected. And for security protocols we also have something like security properties which define if a message or data in a message has properties like integrity or confidentiality. To tackle the vulnerabilities we have seen in communication protocols, we have to tackle each part. But as foundation we need to ensure that no one time errors exist. So we have to make sure that no buffer overflows, integer overflows or something like that are in implementation. By using verification techniques we could do that by program verification. Then when we have this foundation we can look at the messages to ensure that the message formats are correct. We could use functional correctness proofs and with this proofs we can ensure that vulnerabilities like we have seen in Bluebourne or on Heartbleed that these vulnerabilities are prevented. Then at the next level we have also to ensure the protocols in Mantik of course. There are different techniques possible. We could use temporal logic or model checking and when we have also dis-insured then we can prevent errors like seen in SSH. And further step further then we also have to ensure the security properties of security protocols. And therefore we could think of using security protocol proofs to ensure also that implementation fulfills the properties which we want to fulfill it. But let's start at the foundation. Let's look at the absence of runtime errors. So solve this problem. We are using Spark. Spark is a programming language and a verification tool set. And it's especially designed for error avoidance. So this is the reason that Spark contains features like a strong type system and formal contracts. And it's especially also used in this area then. Also the application tool set is able to do a flexible depth of application. So you can prove data and control flows. You can prove dependency contracts. You can even prove that there are no runtime errors exist. Or you can even do more and prove the function correctness of the code. Because of the features it is used in critical projects. So you can think of areas with high safety requirements like aerospace or areas with high security requirements like government or defense area. As it's a compiled language it can also be used for system level programming. And so it's also used in implementation of microcodes. If you're interested in Spark you can find more details on the website of Adaco which still develops these tools. So see the power of Spark is a simple example. We have here a simple z function which calculates absolute value of an integer x. This function mainly consists of an if statement where it is checked that x is greater than zero. If this is the case then x is returned and otherwise the negative value of x is returned. Maybe someone sees already an error there. For the most case it works fine. So we can put some numbers in there and we get the correct number back. But in one case we get not the correct value back. What's the reason for that? The representation of the integer uses the truth complement. And this means that not for all negative numbers we have also a positive counterpart part. So in this case this is the lowest negative number which is possible to see in the end. And if you want to, if you try to negate this value then we get an integer overflow and get at the end back in negative value. If we now implement this function in the same way with Spark we can use the Spark tools to verify if there are any errors exist in the code. The nice thing about this Spark tools is that you don't have to run the code or even compile it. You can just run it on the source code and it will check if there are any errors existing. So in this case at line 6 you see that Spark tools found an error. They also tell us what error is. So they found an overflow check, fail, and also give us a hint what the example is when the event happens. So here it tells us that when x equals integer first then we have an overflow fail. It also gives us a hint what we can do to prevent this error. We could add a precondition here. So this is the function body but the precondition is added to the specification. And you see if we now add a precondition which states that x must not be integer first and then run the Spark tools again. On this function the Spark tools will see that this error will not occur anymore. So you see the Spark tools are able to prevent one-time errors but we can even do more. And that is what we are doing with FACOT Flux. But what is the goal of FACOT Flux? We want to be able to dissect, generate, and verify communication protocols. At the current stage we are focusing on the specification and the parsing of messages but in the future we also want to do more. So FACOT Flux currently consists of a specification language which is able to describe protocol messages. We implemented a parser which is able to parse such a specification and creates an intermediate representation out of it which is then used by a generator to generate Spark code of it. And the Spark code can then be used to verify protocol messages and also parse them. Here is the example. So our specification language is inspired by ETA but we adapted it to fit our purpose. So here in this example we describe a simple message. It's a TS-HARPID message which consists of four fields. So we have a message type field, we have a payload link field, a payload field, and a padding field. The first two fields are fixed in their size and the two fields at the end are variable. We represent such a message by using a message type which is similar to the direct or the swag type in Z. It looks like that. We have just listed all field names and also the type of the field. Then we also have to define of course the type of the field. And then we could now think what would be an adequate type for the message type field at first. So the message type field has a size of one byte so we could think we use just an integer in size of one byte. But that's not really the best use case. So when we look in the specification we will see that only two possible values are valid for message type. And that's one as a HARPID request and two as a HARPID response. So we are using here an enamiration type where we only specify these two possible values. And now if we see a message which does not contain one of these two values we already see that this is not a valid HARPID message. The same I'll be doing with the payload length field. There we also specify restricted integer which only consists of the values from 0 to 2 to the power of 14 minus 20 because that's the size of the payload field. So for the payload and padding field we use here an composite type which is a built-in type which is called payload type. And this just represents a variable size byte array. To make our specification also modular we have to put all types in the name package which is here called TSHARPID. When we look now at the specification it's not really complete as we didn't specify the length constrained for the whole message. And the length constrained of the padding field. So we need to do more. Also what is missing is the relation between the length feed and the payload feed. And this relation is especially important. As we have seen in HARPID that this relation was not respected and so it was possible to send in HARPID request with a high value for the payload length but only in small payload. And then the receiver of such a request has to copy the payload back but did not check if it really fits to the payload that she gets. And so you just read all the data according to the payload length and so read also more data, not also only the message. And this data could be potentially confidential like keys or something like that. So this relation is really important. Here is the full specification of the message. Highlighted are the length expressions in green and the message constraints in orange. Internally we use a representation of our messages in a graph like form. Where each field of the message is represented by a node and the nodes are connected by edges to specify the order of the fields. We can also add further information to edges so we can add length expressions like it is done here between the payload length field and the payload field. And there we specify that the length of the payload field is the value of the payload length field multiplied with 8. Here because the payload length is given in bytes but the length in our specification is given in bit length. We also specify in the same way the length of the padding field by just seeing the padding field as the rest of the message. And we also add restrictions for the message length here. The message length has to be smaller than its value and the padding length has to be at least 16 bytes. This is a rather simple example. We could see the full advantage of our model for more complex protocol messages. So we can also represent optional fields by adding an edge which skips some nodes. We can also represent by a condition that we have some fields which are optionally inserted or also fields which have a different meaning depending on the type. So you could think of ethernet. There you have either type field which is depending on its value interpreted as a length field or as a type field. Here we excerpt of the code which we generate. So all functions which we generate for our message use as input in plain byte array which is then used to do further stuff on it. We generate verification code and access code. The verification code for each method checks that the message is valid until to this point. And if we check that we can then access the value and select the value by the access function. So for example for the message type field we have the message type function and a get message type function. And by using preconditions here we ensure that we first have to check the message type field if it's really a message type and only if it is the case then we can access it. For convenience we have also a function which is quote is valid which checks all fields one by one. And if there's a valid path from the start node to the target node then this function returns to and we can then just access all functions on their own without checking again and again. It's also possible to represent the relation between a payload field and another protocol layer. We can see that payload field under some conditions contain another protocol message and this is also checked at the code level. So therefore we have this is contained predicate here which is a precondition for all functions like you can see. And so we ensure that if a developer or use of the code and reuse it to divide buffer. You can only use a buffer which is labeled correctly as a message in this case like a heartbeat message and so ensure that he does not use the wrong buffer. Let's have a look how we can use the generated code. Here we have a small function where we get the byte array from external source by this virtual read function here. We have to label the buffer here like I already said because we get it from external source is not labeled yet. We have to ensure that it is a buffer which potentially contains a heartbeat message. And only after we have to that done that we can access them the fields of the message. As we already specified the relation between the length and the payload field. The user does not have to access the link field anymore. We have to concentrate on the fields which are really relevant for him which means here the type field and the payload field. But there's still an error here in this code. If you run the Spark tools they will tell us that we cannot just call them like it is here. They tell us that a precondition might fail. What is the reason for that? We did not check the validity. So we have to first check if the field is valid. What we do here with an isValid function and by adding this if statement with a valid function and only accessing the fields. If we get a positive result back we ensure that we only access valid messages. We could alternatively also check each field by one by one and also find out where the error in the message occurred. Looking back what we have achieved so far by using Spark we ensure that no runtime errors exist in our implementation. We have built a tracker flux to also correctly identify if a message is valid. And if this is the case we can also access the fields of the message. In the future we also want to represent the protocol semantics in Wecker Flux and also ensure this part of the protocol. And further down the road we also want to use security protocol proofs to ensure that for security protocols also the security properties are fulfilled in the code which we generate. We will use Wecker Flux for a project which is called QTLS. QTLS is a component based insurance implementation of TLS 1.3. So this project just started this year and is partially funded by the European Union and the state of Saxony. And the essential part of this project is that we want to split the implementation of TLS in critical and non-critical parts. And especially for the critical parts we want to use Spark and Wecker Flux to make sure that they are really correct. As a base platform we want to use the G-Node OS framework but potentially also others will be supported. We see multiple challenges in this project so we have to find out how do we do the separation and get at the end sensible implementation of TLS. How can we prove that implementation at the end is secure? And of course we also want to achieve good performance and also see that implementation has no side channels in it. As the project just started this year there is not much done yet but there is already a repository on GitHub and the source code will also be available in the future. Coming to the conclusion, we have already created a specification language which is powerful enough to specify real-world binary protocols. We already specified ethernet including Vlientax, IPv4 and UDP and are currently working on specifying TLS 1.3. We are able to generate Spark code based on the specification and prove for this generated code that no one-time offers exist and that messages correctly identified as correct or incorrect. Backup flux is still in development so we have found some minor bugs by specifying TLS 1.3 which I am working on currently but the bigger thing which we also want to do is adding the method generation. Currently we can only pass messages but we want also to be able to generate messages based on our specification. After that we also want to be able to specify more protocols. We already looked into USB and there we saw that there are also some features are missing. Currently we are focusing on the TLV method scheme that means that we steadily compute where the field starts and how long the fields are based on other fields and based on length fields. But in some cases this is not possible. So there are protocols where you have to do this at a time time and find out where the next field starts. You can think of areas which contain various sized elements and you have to first pass these elements before you know where the second area starts. But that's something that we also want to support in the future. So at the end also the code of packet flux is available online so if you want to have a look at it or look at the documentation you find it on GitHub. So thank you. Thank you. So are there any questions? Hi. How do you handle hardware specificities like out of Rx execution or reshuffling of instructions? Do you model hardware at all? No, we are not at that level. We are modeling just the messages and generating code should then pass these messages. So you're not working on side channel things? That's something that we want to do in the future also looking at the side channels but that's not currently done yet. Anything else? So thank you.
about the problems we have seen in the communication protocol implementations. And then future. So in the past we have seen multiple security vulnerabilities in communication have BlueBorne that was a set of vulnerabilities millions of devices. And an attacker was able to sensitive data out of another TLS endpoint. low level implementations like Bluetooth or TLS very complex. And implementing complex protocols But as such formal specifications does not exist, we have seen in communication protocols, we have to make sure that no buffer overflows, integer proofs and with this proofs we can ensure that foundation. Let's look at the absence of runtime Spark. Spark is a programming language and a prove the function correctness of the code. there are any errors exist in the code. The nice protocols. At the current stage we are focusing full specification of the message. Highlighted select the value by the access function. So for using Spark we ensure that no runtime errors also access the fields of the message. In the semantics in Wecker Flux and also ensure this which we generate. We will use Wecker Flux for a project is that we want to split the implementation of TLS in critical and framework but potentially also others will be implementation at the end is secure? And of code will also be available in the future. Coming specifying TLS 1.3. We are able to generate Spark want to support in the future. So at the end also