Instructions Unclear:
Undefined Behaviour in Cellular Network Specifications

In this paper, we investigate the presence and impact of undefined behavior in cellular network specifications on modems used in smartphones. In doing so, we found multiple gaps in the LTE specifications that lead to insecure implementations resulting in three high-severity CVEs.

---

This text provides a non-peer-reviewed and more hands-on example of applying our research, focusing on a single use case. I recommend that you read our paper first, to better understand the basic idea, and to get a complete picture of the results.

On undefined behavior

Undefined behavior has been the cause of vulnerabilities throughout the history of computing. Undefined behavior is a behavior for which the specification of a language or system explicitly or implicitly does not state an expected behavior. One of the most prominent cases of undefined behavior in a specification probably are signed integer overflows in the C standard. This allows the compiler to assume that a conforming program will never contain an integer operation that increases said integer beyond it's upper storage boundary of (2^31)-1. This allows compilers implementing the C standard to make compile-time optimizations. However, this has also been the cause of thousands of vulnerabilities. At the time of writing, the NIST CVE database lists 2096 vulnerabilities that are caused by such an integer wrap-around.

While the impact of undefined behavior on programming language standards have been well established, a lot of other specifications have been left out. One of these specifications are cellular specifications. Cellular specifications are the reason your phone works anywhere on the planet: You can board a plane in Germany, fly to the US, disable airplane mode, and your phone will just work, no matter which phone you use, which manufacturer built the cell tower you are connected to or who operates the network behind this cell tower. Cellular specs codify an understanding of how the networks components should interact.

Obviously, the same holds for a lot of network specifications, such as the TCP specification that codifies how computers communicate using the TCP protocol. What makes the cellular specifications special is their scope: They codify everything from the physical properties of communication, such as wave length and modulation to high level interactions, such as procedures for subscriber management. While TCP is concerned with one layer of the ISO/OSI model, cellular specs deal with all of these layers, often in a tightly coupled way.

Our initial assumption was that there is likely quite a lot of undefined behavior in cellular specifications; but finding it just from reading the specifications is rather impractical: We would likely miss a lot of undefined behavior, and the approach would also not be reproducible at all. The latter, however, is of quite a large importance: We will only be able to look at small parts of the specification, and if anyone in the future wants to look at other parts of the specification that deal with functionality different from what we looked at, we want to enable doing this in an understandable and repeatable way.

There is also another practical aspect to this research project: If we find undefined behavior in the specification, we can only speculate if this led to exploitable vulnerabilities when implemented.

We thus faced two challenges: Systematically finding undefined behavior in the behemoth of a text document that is the cellular specification, and measuring the real-world impact of undefined behavior.

Before we are going to look at any of this, we will have a brief look at the Public Warning capabilities of cellular networks and serving as a running example. In our paper, we also investigate SMS and RRC, a protocol used to establish and secure the connection between phone and cell tower.

Public Warning System in LTE

You might have heard about Wireless Emergency Alerts (US), EU-Alert (European Union) or the Earth Quake and Tsunami Warning System (Asia). All of these are names for the functionality of cellular networks used to alert mobile phone users in a specific area of natural disasters and other health hazards. If you have never seen a phone receive such an alert: my colleague Merlin created a demo video.

As cellular networks might be overwhelmed during natural disasters by large numbers of users attempting to contact emergency services (or friends and family members), the public warning system has been designed to scale in a way that a) is not influenced by the number of phones connected to a cell tower and b) even works if the network is so overwhelmed that normal data transmission is no longer possible.

To do so, in case of emergency, the cell tower periodically broadcasts the hazard warning unidirectionally. This makes it fundamentally different from SMS or Messenger services: The cell tower does not send the hazard warning to a specific phone. Instead, it sends it in a way that every phone in the vicinity can pick-up the message; similar to how conventional AM/FM radio works. Thus, it even works if your phone is not registered with the network, for instance, because it is missing a SIM-card, and, more crucially, it does not matter how many phones are within the range of the cell tower - the required bandwidth and computational resources stay the same. This also reduces the load on the core network connecting the different cell towers, compared to SMS: It only has to contact the tower once instead of contacting it for every phone that should receive the SMS.

If you know IP multicast, this might sound familiar: if you send an IP packet to a multicast IP address, then every PC within the subnet will receive this packet and the packet multiplexing only happens as close to the edge as possible. However, there is a crucial difference. Aside from differences arising because Ethernet typically does not share one medium/cable for the final connection between the edge switch and the PC, multicasting happens once. If you send an IP multicast packet, and there are two systems within this subnet, both systems will receive this message. If then a third system joins the subnet, it will never receive this packet. However, that would be a bad solution for hazard warnings: If your phone was off when a hazard alert was originally sent, or you just entered the hazard area, then you would not receive a message. For that reason, hazard messages are sent periodically. However, that creates a new problem: Everyone's phone receives the same message multiple times, once for each repetition, potentially for hours on end. To avoid the alarm going off for each received message, a deduplication mechanism had to be implemented.

Speaking of implementation: There are multiple separate specification documents describing how public warning systems are to be implemented in cellular networks, one for each generation. The concrete implementation varies a bit between generations. We will focus on the LTE implementation, as that has wide adoption (compared to e.g., 3G networks that are being disbanded to free up the used frequencies) as well as excellent tooling support for the implementation of our PoC later on.

Technical details on the Public Warning System in LTE

We will now have a brief look at how hazard alerts are implemented in LTE networks. While there are quite a few components involved in a real network, only two matter to us for now: The cell tower (also called eNodeB, eNB) and the mobile phone (also called User Equipment, UE). When the cell tower is instructed to send a hazard warning by its network operator, it does so by utilizing the broadcast channel (BCCH). Usually, the BCCH is used to periodically broadcast general cell information, such as a list of networks that are available on this cell, to all UEs in receival range. This information is sent in packages called System Information Blocks (SIBs). SIB type 1 (SIB1) contains a list of all SIBs that are being transmitted at the moment, and in what time slot they are sent. This schedule is used by the UEs to ensure that they are in receival mode when the other SIBs are broadcasted. Of particular interest to us is SIB type 12, which carries PWS hazard messages.

Let us take a look at the contents of this SIB. SIB processing in LTE is specified in TS36.331. In particular, on page 350, we can find the following ASN.1 description of the contents of SIB12:

SystemInformationBlockType12-r9 ::= SEQUENCE {
    messageIdentifier-r9 BIT STRING (SIZE (16)),
    serialNumber-r9 BIT STRING (SIZE (16)),
    warningMessageSegmentType-r9 ENUMERATED {notLastSegment, lastSegment},
    warningMessageSegmentNumber-r9 INTEGER (0..63),
    warningMessageSegment-r9 OCTET STRING,
    dataCodingScheme-r9 OCTET STRING (SIZE (1)) OPTIONAL, -- Cond Segment1
    lateNonCriticalExtension OCTET STRING OPTIONAL,
    ...
}

This ASN.1 definition tells us that every SIB12 has five mandatory fields (in blue and yellow), one optional field to transmit the data encoding information, and a placeholder for later extensions. Message identifier and serial number are used for deduplication and to signal hazard severity. Each complete message with the same id and serial is only displayed once every 24 hours, to avoid an alarm going off on each periodical transmission of hazard alerts. The severity is used by the UE to determine if a message is to be ignored (test severity), or if an alarm sound has to be played even if the phone is in silent mode (very high hazard severity). We will ignore those two in our example from now on - a full example on how to handle these can be found in our paper's artifact.

Whats of interest in this tutorial are the segment type, segment number, and the segment itself. During the transmission of a hazard message, the cell tower will split the text of the hazard message to fit into the size of an SIB, which depends on the network's configuration and the used encoding. Each of these segments is then transmitted using a separate SIB.

• The segment contains the text fragment that is being transmitted. The text is not transmitted using ASCII encoding but usually uses a special GSM 7 bit encoding, which we ignore for exemplary reasons here.
• The segment number is used to order the text fragments. As the SIBs are transmitted periodically, they might be received out of order, e.g. because the UE joined the cell in the middle of a transmission. The segment number is then used to reorder the fragments.
• The segment type is set to lastSegment for the final segment with the highest segment number, and set to notLastSegment otherwise.

This is illustrated in the example below, which is based on the reassembly procedure that we reverse-engineered from MediaTek's 4G modem firmware. In this sample, the text "BALLISTIC MISSILE THREAT INBOUND TO HAWAII" is split up into two segments. "INBOUND TO HAWAII" is received first, followed by "BALLISTIC MISSILE THREAT". Since "INBOUND TO HAWAII" has the lastSegment flag, the baseband knows that this is the final fragment, and also knows that it has to await one more segment since this the second fragment and thus the first fragment is still missing. Only after the first fragment is received as well are the two concatenated and forwarded to Android to be displayed.

This is the defined behavior of the public warning system in LTE. But what if the cell tower does not send a benign message but instead attempts to transmit bogus messages, purposefully crafted to not adhere to the specification, or due to a bug? To determine if there are such messages for which the correct course of action for the UE is not defined, we need a way of systematically evaluating the specification for such gaps.

Formal models and undefined behavior

While one could attempt to look at the textual description of the PWS system in TS36.331 very carefully and determine potential gaps, this would not be a systematic way of conducting such an analysis. After all, the chance of missing an edge case is rather high, as there are absolutely no guarantees on the completeness of such a manual evaluation. Instead, we aim to do this in a formal, tooling-assisted way.

To do so, we are going to model the defined behavior of the public warning system in a state machine. A state machine consists of two things: States and transitions. In our case, each state represents a possible combination of previously received SIB12s. That is equivalent to the "Baseband memory" in the animation above, just that we are not modeling a specific implementation but an abstract scenario. Transitions within a state machine define into which state the system can go from the current state, and under what condition. Our conditions here are the different SIB12s that we could receive.

If we only care about our three yellow fields, and disregard the segments text (as the text itself is irrelevant to how the text is going to be reassembled), we need to store the segment numbers, and segment types of all previously received and fragmented SIB12s in the state. For each of the 64 possible segment numbers, we could have received an SIB12 that was notLastSegment or lastSegment. We could also have previously received two SIB12 with the same segment number, but one being the lastSegment and the other not being the last segment. Finally, we could also ave not received an SIB12 with this segment number at all. We can thus calculate the number of possible states: We have four different receival states for each segment number, to the power of 64 different segment numbers. However, not all of these states are reachable: For instance, we cannot reach a state where we have stored an SIB12 that is the first segment and has the lastSegment flag set, together with any other SIB12. That is because if we receive a SIB12 with segment number 0, which is the last segment, this SIB12 does not require reassembly and can be immediately displayed.

Figuring out which states are reachable and defining all those states (let alone the 128 potential outgoing transitions each state could have) is impractical. Instead, we need a way to describe our system without explicitly enumerating each state.

Using TLA+ to model our problem

To do so, we use a language called TLA+. In the words of it's author, Leslie Lamport:

TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.

In simple terms, TLA+ allows us to model the behavior of the UE, as defined in the specification, and then use a tool called "tlc" to perform model checking.

In the first step, we are now going to model the defined behavior of receiving PWS messages. You will need the TLA+ CLI tools or the TLA+ extension for VSCode to follow along and perform model checking. For this tutorial, I assume you are using tla-bin.

We now need to create two files: pws.cfg will be our configuration file, while pws.tla will contain the actual model. The configuration file primarily tells the model checker where the specification is stored. In our case, our model will contain a Spec variable containing this specification. This is then the "entrypoint" in our model. The configuration also tells the model checker where the invariant is stored. The Invariant is evaluated after every transition, with the goal of finding a series of state transitions that violate the invariant.

SPECIFICATION Spec
INVARIANT Invariant

We can now move on to actually writing our model. In order to understand the syntax we are going to use, I recommend reading the Learntla+ pages on operators and structured data before continuing.
We will start with the following rather empty model to be stored as pws.tla:

------------------------------- MODULE pws -------------------------------
EXTENDS Integers, TLC, FiniteSets, Sequences
VARIABLES buffer

ValidPDUs == [
    warningMessageSegmentTypeR9: {0,1},
    warningMessageSegmentNumberR9: 0..63
]

Init == /\ buffer = {}
Invariant == TRUE

Spec == Init
===========================================================================

Here is how this works:

• First, we import several packages that we will need later via EXTENDS
• Then we declare a variable called buffer. This will be a set in which we store the previously received but unassembled packages.
• Then we define a set ValidPDUs. These are all syntactially valid SIB12s that exist. Segment type 0 corresponds to notLastSegment, while segment type 1 corresponds to lastSegment.
• Init contains our initial configuration; in our case an empty buffer.
• Then we declare our Invariant. For now this will be TRUE.
• Lastly, we declare our specification, which for now only contains that we want the initial relation to be present.

You can now model check this by running tlc pws, which should give you:

Finished computing initial states: 1 distinct state generated at xxx.
Error: No next state actions defined to generate successor states from.

Sounds about right since we have not declared any transitions ("state actions") originating from our initial state. This is what we are going to do next.

Receiving unfragmented PDUs

To understand which state transitions we need to model, we need to determine what scenarios we need to cover. In other words: Which incoming PDUs could there be, and what would we have to do with them? To do so, we need to look at the specification for SIB12 processing TS36.331, section 5.2.2.19. We start with the first scenario described there:

Upon receiving SystemInformationBlockType12, the UE shall:

• if the SystemInformationBlockType12 contains a complete warning message:
  • forward the received warning message, messageIdentifier, serialNumber and dataCodingScheme to upper layers
  • continue reception of SystemInformationBlockType12;

That is the most simple case: We receive a PWS hazard message thats just a single segment. In that case we do not need to buffer (and instead "forward the received warning message [...] to upper layers"). The criteria for such a PDU are very simple: It must be the first segment, so the segmentNumber must be 0, and it must be the last segment, so the segmentType must be 1 (corresponding to lastSegment). To model this, we create two new operators in our TLA+ file: RecvComplete_1(r) and RecvCompletePre_1(r). If you are coming from a programming background, then you can think of Operators as "functions". RecvComplete_1(r) will handle the reception of the PDU r (which will come from the ValidPDUs set that we introduced earlier), in case it is an unfragmented message. To check for this condition, it will internally use RecvCompletePre_1(r). Codifying the above constraints, RecvCompletePre_1(r) looks like this:

RecvCompletePre_1(r) == /\ r.warningMessageSegmentTypeR9 = 1
                        /\ r.warningMessageSegmentNumberR9 = 0

This operator returns true if the segment type is 1 and the segment number is 0, so we have an unfragmented PDU. We now need to write the operator that handles this case. Since we already know that we do not need to do anything but "forwarding", which is outside of our model and does not modify the buffer, this implementation is rather simple:

RecvComplete_1(r) == /\ RecvCompletePre_1(r)
                     /\ UNCHANGED buffer

This is evaluated as follows: If RecvCompletePre_1(r) is true, so the precondition for "we receive an unfragmented message" is met, then the buffer remains unchanged (which is always true). If the first part of the conjunction is false, then the second part is never evaluated. We will integrate this into the overall model later on, and now continue with the other possible PDUs that we can receive.

Continuing an existing message reassembly processabc

We can now get back to TS36.331, section 5.2.2.19 and continue with the next condition listed in there, which covers reassembly of a message for which we already have received one or multiple fragments:

• else:
  • if the received values of messageIdentifier and serialNumber are the same (each value is the same) as a pair for which a warning message is currently being assembled:
    • store the received warningMessageSegment;
    • if all segments of a warning message have been received:
      • assemble the warning message from the received warningMessageSegment;
      • forward the received warning message, messageIdentifier, serialNumber and dataCodingScheme to upper layers;
      • stop assembling a warning message for this messageIdentifier and serialNumber and delete all stored information held for it;

We can ignore the condition on message identifier and serial, since our simplified model does not contain them. We just assume that there is only one possible combination of identifier and serial, so the condition is equivalent to "if there is a message being assembled" which can be boiled down to "if there is something in the buffer". The implementation of the operators for this transition is a bit more complicated. The specification talks about a warning message that is "being assembled" and then checks if "all segments have been received". However, there is no clear explanation of what this means and which conditions we need to check to determine if a message is (in)completely received. Instead, we take a constructive approach. Let's think about what a complete message looks like: If a message has i segments, then we will have (i-1) segments with segment numbers from 0 to (i-1) that are notLastSegment, and the final segment that has segment number i. So the set of all possible complete messages looks like this:

CompleteSequences == {
    [
        warningMessageSegmentTypeR9: { 0 },
        warningMessageSegmentNumberR9: 1..(i-1)
    ] \union {[
        warningMessageSegmentTypeR9 |-> 1, 
        warningMessageSegmentNumberR9 |-> i
    ]} 
    : i \in 1..63
}

What we are doing here is constructing a set of sets: Each "inner" set contains i segments that can be reassembled by the rule we established above, and the outer set generates these inner sets for 2 to 64 segments. We can now use this to check if our buffer contains a complete set, if we would add a received message r to it by checking if the union of those is in our set of all possible complete message sequences.

IsComplete(r) == (buffer \union {r}) \in CompleteSequences

We can also use this to check if we need to receive further message segments to be able to reassemble the message, by introducing another operator IsIncomplete(r):

IsSubset(a, b) == a \subseteq b /\ a /= b 
IsIncomplete(r) == \E x \in CompleteSequences:
                      IsSubset((buffer \union {r}), x)

Essentially IsIncomplete(r) checks if there is any complete message sequence that is a true superset of the union of the current buffer and our received message r. Please note that the negation of IsComplete is different from IsIncomplete: There might be (and in fact there are) message sequences that cannot be completed, and by our logic, they are neither complete nor incomplete. The beauty of our way of constructing these checks lies in the fact that we never need to define constraints with regard to our received message r; we do not need to think about any edge cases. Instead, we construct defined behavior (complete messages) and base all conditions on this. We can now use these new operators to implement our state transitions. We have to cover two cases:

• Either we receive a fragment but do not have all segment for this message yet, in which case we need to store this segment. We will use IsIncomplete(r) to determine if this is the case
• Or we receive a segment and that was the last missing segment, which prompts a reassembly. We will use IsComplete(r) to detect this scenario. After reassembly, we remove everything from the buffer.

Firstly, we implement the preconditions for the state transition:

ContExistingPre_2(r) ==  /\ ~RecvCompletePre_1(r)
                         /\ Cardinality(buffer) > 0
                         /\ IsComplete(r) \/ IsIncomplete(r)

There are three parts to this: First we ensure that our received message r does not match the criteria of an unfragmented message, which we handled previously. Then we check if we are currently assembling a message. Finally, we check that either or completeness or our incompleteness criteria is fulfilled.

Finally, we can specify the transition operation itself. This is now pretty straightforward: We check if we can take this action by verifying it's preconditions, then we either store the received segment r in our buffer if we are still incomplete, or we clear the buffer ("delete all stored information held for it" in the words of the specification) if we have received all required segments.

ContExisting_2(r) ==  /\ ContExistingPre_2(r)
                      /\ \/ /\ IsIncomplete(r)
                            /\ buffer' = buffer \union {r}
                         \/ /\ IsComplete(r)
                            /\ buffer' = {}

Receiving new messages

Lastly, we need to implement the final case covered by the specification:

else if the received values of messageIdentifier and/or serialNumber are not the same as any of the pairs for which a warning message is currently being assembled:

• start assembling a warning message for this messageIdentifier and serialNumber pair;
• store the received warningMessageSegment;
• continue reception of SystemInformationBlockType12;

Again, we can ignore the part about messageIdentifiers and serialNumbers. So what we effectively need to implement: If none of the previous cases match, and the buffer is empty (because we are currently not assembling a message), then we need to store the received message:

RecvNewPre_3(r) == /\ ~RecvCompletePre_1(r)
                   /\ ~ContExistingPre_2(r)
                   /\ Cardinality(buffer) = 0
RecvNew_3(r) == /\ RecvNewPre_3(r)
                /\ buffer' = { r }

Putting it all together

Finally, we can use our new operators to extend our state machine. To do so, we extend our specification with an operator called Next that contains the logic for state transitions. This operator will be verified temporally for each "step". In our case, a "step" is the reception of a message segment r, drawn from the set of all possible segments ValidPDUs.

Next == /\ \E r \in ValidPDUs:
    \/ RecvComplete_1(r)
    \/ ContExisting_2(r)
    \/ RecvNew_3(r)

We also need to modify the Spec to reflect the introduction our next-state operator. We use the [][Next] syntax to specify that we want the operator Next to hold for every step into the future.

Spec == Init /\ [][Next]_<<buffer>>

This is how your .tla file should look like now:

------------------------------- MODULE pws -------------------------------
EXTENDS Integers, TLC, FiniteSets, Sequences
VARIABLES buffer

MaxSegmentNumber == 63

ValidPDUs == [
    warningMessageSegmentTypeR9: {0,1},
    warningMessageSegmentNumberR9: 0..MaxSegmentNumber
]

CompleteSequences == {
    [
        warningMessageSegmentTypeR9: { 0 },
        warningMessageSegmentNumberR9: 0..(i-1)
    ] \union {[
            warningMessageSegmentTypeR9 |->: 1,
            warningMessageSegmentNumberR9 |->: i
    ]} 
    : i \in 1..MaxSegmentNumber
}

Init == /\ buffer = {}
Invariant == TRUE

RecvCompletePre_1(r) == /\ r.warningMessageSegmentTypeR9 = 1
                        /\ r.warningMessageSegmentNumberR9 = 0
RecvComplete_1(r) == /\ RecvCompletePre_1(r)
                        /\ UNCHANGED buffer

IsSubset(a, b) == a \subseteq b /\ a /= b
IsComplete(r) == (buffer \union {r}) \in CompleteSequences
IsIncomplete(r) == \E x \in CompleteSequences:  IsSubset((buffer \union {r}), x)

ContExistingPre_2(r) ==  /\ ~RecvCompletePre_1(r)
                         /\ Cardinality(buffer) > 0
                         /\ IsComplete(r) \/ IsIncomplete(r)

ContExisting_2(r) ==    /\ ContExistingPre_2(r)
                        /\ \/ /\ IsIncomplete(r)
                            /\ buffer' = buffer \union {r}
                        \/ /\ IsComplete(r)
                            /\ buffer' = {}

RecvNewPre_3(r) ==  /\ ~RecvCompletePre_1(r)
                    /\ ~ContExistingPre_2(r)
                    /\ Cardinality(buffer) = 0
RecvNew_3(r) == /\ RecvNewPre_3(r)
                /\ buffer' = { r }

Next == /\ \E r \in ValidPDUs:
                \/ RecvComplete_1(r)
                \/ ContExisting_2(r)
                \/ RecvNew_3(r)

Spec == Init /\ [][Next]_<:<:buffer>:>:
=============================================================================

If we now check this specification via tlc pws, then we are greeted by a deadlock detected by the model checker:

Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: 
buffer = {}

State 2: 
buffer = {[warningMessageSegmentTypeR9 |-> 0, warningMessageSegmentNumberR9 |-> 63]}

What is happening here is that once we receive a segment that has the highest possible segment number but is not a last segment, that this segment is never received from the buffer. Lets see what the specification says about such a scenario.

The UE should discard warningMessageSegment and the associated values of messageIdentifier and serialNumber for SystemInformationBlockType12 if the complete warning message has not been assembled within a period of 3 hours

Therefore, this segment would be discarded after a few hours in a real phone. There is a way to implement such a timer in TLA+ (and we explain this in our paper, if you are curious), but lets ignore this for now and disable deadlock checks by running tlc -deadlock pws. However, now model checking takes quite a while, as the model checker has to exomplore every valid buffer configuration for up to 63 segments in the buffer. To speed things up, let us reduce the amount of different segments we can receive to 5. You might have noticed that I introduced a variable MaxSegmentNumber in the code sample above to make this convenient. Set MaxSegmentNumber = 4 (segment numbers are 0-indexed) and rerun tlc -deadlock pws. Now the model checking will, hopefully, be sucessful.

From defined to undefined behavior

So far, our model models the defined behavior of the PWS specification. If we encounter a PDU r for which none of the preconditions become true, then RecvComplete_1(r) \/ ContExisting_2(r) \/ RecvNew_3(r) is false, and the next PDU will be drawn. That is not what we want. If there is no defined transition upon the reception of a specific PDU in some state, then this is, by definition, undefined behavior. We thus want that for EVERY PDU there is a possible transition in every state the system could be in, or the model checking should fail. So we need to ensure that in such a case the term inside the existence quantifier will become true. To achieve this, we make the following adjustment:

Next == /\ \E r \in ValidPDUs:
        \/ RecvComplete_1(r)
        \/ ContExisting_2(r)
        \/ RecvNew_3(r)
        \/  /\ ~RecvCompletePre_1(r)
            /\ ~ContExistingPre_2(r)
            /\ ~RecvNewPre_3(r)
            /\ PrintT(r)

This way, either one of the first three disjunctions is true, or the last element in the disjunction is true. However, we do not attach a behavior for this scenario to our specification. Instead, we tell tlc to print the value of r. This way, we specify a transition in which we do not update the buffer, nor do we specify that the buffer should remain unchanged. This is considered an invalid scenario by the model checker, and it throws an error once this situation is encountered. This is equivalent to adding transitions into the "undefined state" as explained in section 3.3 of our paper.

If you now rerun tlc -deadlock pws again, you will see that precisely this condition is triggered, as tlc throws another error:

Error: The behavior up to this point is:
State 1: <Initial predicate>
buffer = {}

State 2: <Next line 51, col 9 to line 58, col 32 of module pws>
buffer = {[warningMessageSegmentTypeR9 |-> 0, warningMessageSegmentNumberR9 |-> 0]}

[warningMessageSegmentTypeR9 |-> 0, warningMessageSegmentNumberR9 |-> 4]
State 3: <Next line 51, col 9 to line 58, col 32 of module pws>
buffer = null

This is the same message sequence as above, but not because of a deadlock, but because a message with [warningMessageSegmentTypeR9 |-> 0, warningMessageSegmentNumberR9 |-> 4] cannot be completed and is undefined behavior. In this case, the sequence that triggered this was as follows:

As you can see, tlc generated a concrete counter-example that leads to undefined behavior caused by the reception of a segment with the highest possible segment number that is not signaled to be a last segment and, as a consequence, cannot be reassembled. Assuming you have the required equipment (SDR, shielding box, programmable SIM card), you could now use a physical setup to see how a real smartphone modem reacts to this. I hope that this guide helped in understanding our method, and that it might help reproduce our findings or extend our work.

If you have any further questions, remarks, or ideas, feel free to drop me an e-mail.