RFC 963
Some problems with the specification of the Military Standard Internet Protocol
RFC 963: Some Problems with the Specification of the Military Standard Internet Protocol 🎀
Okay bestie, so this is RFC 963 💖 It was written by Deepinder P. Sidhu from Iowa State University, and it's dated November 1985. It's a little memo that says its whole purpose is to share helpful info, and the header doesn't say it obsoletes or updates any other RFC. Nothing to hunt down there 🧚
Status of This Memo 🌸
The point of this RFC is to give you useful info about the Military Standard Internet Protocol (MIL-STD-1777), so you can actually build a reliable implementation of that protocol standard. Distribution of this note is unlimited, so share it with everyone 💅
Abstract ✨
This paper calls out several big problems in the spec for the Military Standard Internet Protocol (MIL-STD-1777, dated August 1983 [MILS83a]). It's based on a first pass through the protocol standard, and the problems are:
- fragmented messages don't get fully reassembled 💀
- a state transition is missing
- the test for whether reassembly is finished is wrong
- the fragment sizes are computed wrong
- there are minor errors in message reassembly
- certain datagrams get the wrong computed length
The note also proposes fixes for all of these 🔥
1. Introduction 🦋
Okay so, the last few years have been a glow-up for tools that help build reliable communication protocols. They help with specifying, verifying, implementing, and testing protocols, and a bunch of protocols have already been analyzed and built with them. Some examples of automated verification and implementation of real-world protocols are in [BLUT82] [BLUT83] [SIDD83] [SIDD84] 📚
We're currently working on automatically implementing the Military Standard Internet Protocol (IP). This analysis is based on the published IP specification [MILS83a], dated 12 August 1983 ✨
And here's the tea. While we were studying the MIL Standard IP spec, we spotted tons of errors in it. One result is that the protocol will never deliver fragmented incoming datagrams. If you fix that error, those datagrams will be missing some data and their lengths will be reported incorrectly 😭 On top of that, outgoing datagrams that get split into fragments will be missing some data too. We'll prove all of this from the IP spec [MILS83a] below 🙈
2. Internet Protocol 🌈
So, the Internet Protocol (IP) is a network layer protocol in the DoD protocol hierarchy. It gives you communication across interconnected packet-switched networks in an internetwork environment. IP is a pure datagram service, which means it has no mechanism for reliability, flow control, sequencing, etc. 🫶
Those features come from a connection-oriented protocol called DoD Transmission Control Protocol (TCP) [MILS83b], which runs in the layer above IP. TCP is designed to work over channels that are inherently unreliable, meaning channels that can lose, damage, duplicate, and reorder packets. Iconic behavior from TCP honestly 👑
Over the years, DARPA has backed several versions of IP, and the most recent one appeared in [POSJ81]. A few years ago, the Defense Communications Agency decided to standardize IP for use in DoD networks. To make that happen, the DCA supported a formal specification of the protocol, following the design in [POSJ81] and the technique and organization defined in [SDC82]. The detailed spec, given in [MILS83a], was adopted as the DoD standard for the Internet Protocol 🎉
Now the state transitions. The IP spec organizes them into decision tables. The decision functions and action procedures are written in a subset of Ada[1], and they may use a set of machine-specific data structures. Decision tables are provided for these pairs of state name and interface event:
<inactive, send from upper layer><inactive, receive from lower layer><reassembling, receive from lower layer>
There's also a decision table for <reassembling, reassembly time limit elapsed>, so the protocol can raise an error when some fragments of a datagram arrived but others are missing 🚨 (Heads up: the event names are English descriptions, not the names used in [MILS83a].)
3. Problems with MIL Standard IP 💅
Splitting datagrams into fragments when they can't go over a subnetwork in one piece, and then putting them back together, is one of IP's major jobs. The spec has several problems in this area, and the most serious one is that it fails to insert the last fragment of an incoming datagram. That means datagrams get handed up to the upper-level protocol (ULP) with some data missing 💔 Another error here is that the wrong data length gets passed to the ULP for reassembled datagrams, and the consequences are unpredictable.
Okay, plot twist. As the spec [MILS83a] is currently written, these errors barely matter, because the test for reassembly completion will always fail. So reassembled datagrams never get delivered at all 🙃
A missing row in one of the decision tables also means that network control (ICMP) messages arriving in fragments will never get processed. Other errors include a few bytes possibly getting thrown away from each transmitted fragment, and some statements that cause run-time exceptions instead of doing what they're supposed to do 😬
The biggest general problem is that the program language and action table parts of the spec were clearly never run through any automatic syntax checker. Variable and procedure names are sometimes misspelled, and the syntax of the action statements is often wrong. We list some of these as cautionary notes for implementors, but we don't claim it's the full list. We only talk about syntax errors when they show up alongside other problems 🧚
The next section digs into some of the serious errors we found in the MIL standard IP [MIL83a] during our initial study, and we also propose corrections for each one ✨
4. Detailed Discussion of the Problems 🔍
Problem 1: Failure to Insert Last Fragment 💖
This problem lives in the decision table for the state reassembling and the input "receive from lower layer" [MILS83a, sec 9.4.6.1.3]. It shows up in this row of the table:[2]
________________________________________________________
check- SNP TTL where a reass ICMP
sum params valid to frag done check-
valid? valid? ? ? ? ? sum?
__________________________________________________________________
YES YES YES ULP YES YES d reass_
delivery;
state :=
INACTIVE
__________________________________________________________________So reass_done returns YES when the fragment just received is the last one needed to build a complete datagram, and NO otherwise. The action procedure reass_delivery just hands a fully reassembled datagram up to the upper-level protocol. The procedure that actually slots an incoming fragment into the datagram being built is reassemble. This row never calls reassemble, so every incoming fragmented datagram gets delivered to the upper layer with one fragment missing 😭 The fix is to rewrite the row like this:
________________________________________________________
check- SNP TTL where a reass ICMP
sum params valid to frag done check-
valid? valid? ? ? ? ? sum?
__________________________________________________________________
YES YES YES ULP YES YES d reassemble;
reass_
delivery;
state :=
INACTIVE
__________________________________________________________________Also, the name reass_done is kind of a mess 🙈 When that function gets called, datagram reassembly definitely hasn't finished yet, so the name is misleading. A better name would be last_fragment.
Problem 2: Missing State Transition 🦋
This one is about a row that's just missing from the same decision table [MILS83a, sec 9.4.6.1.3]. Incoming packets either go to an upper-level protocol (ULP), or they're network control messages, which are marked ICMP (Internet Control Message Protocol). Once control messages are completely assembled, an IP procedure called analyze processes them. The decision table has this row:
________________________________________________________
check- SNP TTL where a reass ICMP
sum params valid to frag done check-
valid? valid? ? ? ? ? sum?
__________________________________________________________________
YES YES YES ICMP YES NO d reassemble;
__________________________________________________________________But it has no entry for the case where where_to returns ICMP, a_frag returns YES, and reass_done returns YES. An extra row should go in, reading:
________________________________________________________
check- SNP TTL where a reass ICMP
sum params valid to frag done check-
valid? valid? ? ? ? ? sum?
__________________________________________________________________
YES YES YES ICMP YES YES d reassemble;
analyze;
state :=
INACTIVE
__________________________________________________________________Without this row, incoming fragmented ICMP messages will never get analyzed. The state machine has no action defined for when the last fragment arrives, so those messages just sit there 😬
Problem 3: Errors in reass_done ✨
The function reass_done, as you can see from the above, decides whether the incoming subnetwork packet is the last fragment needed to finish reassembling an IP datagram. To understand the errors in this function, we first have to understand how it uses its data structures 🧚
Okay bestie, so the reassembly bit map is kept separately for each state machine 🗺️✨ Here's the catch: each bit doesn't stand for one fragment. It stands for a block, which is 8 octets 🧩 Fragments can be all different lengths, so counting in blocks keeps things tidy. Every fragment except the "tail" one (more on that in a sec) is a whole number of blocks. Each fragment's offset from the start of the datagram is in blocks, and it lives in a field in each incoming packet's header 📦 The total length of a fragment (header included) goes in total_length, measured in octets. The header length goes in header_length, measured in words, where a word is 4 octets 💅
Now the tricky part is that there are two different "last" fragments, and mixing them up is how you get chaos 😭 The last fragment is the one that arrives last in time, so it's the one that finishes reassembly. The tail fragment is the one that sits last in the datagram itself, spatially. Its length and offset tell you the total length of the whole datagram, and the code works that out in the action procedure reassembly, saving it in total_data_length. If the tail fragment hasn't shown up yet, that value is just treated as zero 🫶
The function reass_done [MILS83a, sec 9.4.6.2.6] decides whether an incoming fragment is the last one, and it goes like this:
- If the tail fragment hasn't been received before and the incoming fragment isn't the tail fragment, return NO.
- Otherwise, if the tail fragment hasn't been received but the incoming fragment is the tail fragment, check whether every fragment spatially before the tail has also been received.
- Otherwise, if the tail fragment was received earlier, check whether the incoming fragment is the one still needed to finish reassembly.
Case (2) is handled by this statement (yes, it's a little messy 🙈):
if (state_vector.reassembly_map from 0 to
(((from_SNP.dtgm.total_length -
(from_SNP.dtgm.header_length * 4) + 7) / 8)
+ 7) / 8 is set)
then return YES;The + 7 ) / 8 bit shows up twice, and that's almost certainly a misprint 🙃 The function f(x) = (x + 7) / 8 turns octets into blocks and rounds any leftover upward, so doing it twice is unnecessary. The second problem is that the fragment_offset field of the incoming packet gets ignored. The tail fragment only tells you its own length, not the length of the whole datagram. To get the whole thing, you have to add the tail fragment's offset to its own length 🧠 The third problem is the meaning of "... from ... to ..." 👀 If it works like the .. range in Ada [ADA83, sec 3.6], meaning both bounds are included, then you need to subtract 1 from the final expression.
So the expression after to should change to:
from_SNP.dtgm.fragment_offset +
((from_SNP.dtgm.total_length -
(from_SNP.dtgm.header_length * 4) + 7) / 8) - 1Case (3) has its own serious problem 😤 Here the relevant statement is:
if (all reassembly map from 0 to
(state_vector.total_data_length + 7)/8 is set
then return YESIf the tail fragment came in earlier, this code asks whether every bit in the reassembly map is set. That won't be true even when the incoming fragment is the last one, because reassembly, which is what actually sets those bits, hasn't run for this fragment yet. So the statement has to skip over the bits belonging to the incoming fragment. Depending on whether those bits sit at the start of the map or in the middle (the end case was already covered above), the range needs to account for that. The statement should be changed to read:
if from_SNP.dtgm.fragment_offset = 0 then
if (all reassembly map from
from_SNP.dtgm.fragment_offset +
((from_SNP.dtgm.total_length -
from_SNP.dtgm.header_length * 4) + 7) / 8
to ((state_vector.total_data_length + 7) / 8 - 1) is set)
then return YES;
else return NO;
end if;
else
if (all reassembly map from 0 to
(from_SNP.dtgm.fragment_offset - 1) is set)
and (all reassembly map from
from_SNP.dtgm.fragment_offset +
((from_SNP.dtgm.total_length -
from_SNP.dtgm.header_length * 4) + 7) / 8
to ((state_vector.total_data_length + 7) / 8 - 1) is set)
then return YES;
else return NO;
end if;
end if;Note that the upper bound needs the - 1 here too, same as before 🔁
Problem 4: Errors in fragment_and_send ✨
The action procedure fragment_and_send [MILS83a, sec 9.4.6.3.7] breaks up datagrams that are too big to go through the subnetwork as one packet 📦 The specification requires [MILS83a sec 9.2.2, sec 9.4.6.3.7] that each fragment, except possibly the "tail" fragment, contain a whole number of 8-octet groups (called "blocks"). On top of that, each fragment has to start on a block boundary 🧱
In the algorithm for fragment_and_send, every fragment except the tail is the same size, and the procedure starts by working out that size with this statement:
data_per_fragment := maximum subnet transmission unit
- (20 + number of bytes of option data);Apart from forgetting to allow for header padding (which the next section covers), this line has a serious error: it never makes sure the result is a multiple of the block size, which is 8 octets 😱 The result would be that up to seven octets per fragment never get sent at all. To fix that and to allow for header padding, the statement should be changed to:
data_per_fragment := (maximum subnet transmission unit
- (((20 + number of bytes of option data)+3)/4*4)/8*8;Another issue is that the procedure doesn't handle the case where the length of the data is an exact multiple of eight 🙈 The procedure has these statements:
number_of fragments := (from_ULP.length +
(data_per_fragment - 1)) / data_per_fragment;
data_in_last_frag := from_ULP.length modulo data_per_fragment;(In our terminology, data_in_last_frag would be renamed data_in_tail_frag. Also, the proper spelling of the Ada operator is mod [ADA83, sec 4.5.5].)
If data_in_last_frag is zero, things go wrong fast 💀 One possible result is that the datagram gets split into one more fragment than it needs, with the tail fragment holding no data bytes. The assignment of data into that tail fragment would still "succeed," written as:
output_data [i..i-1] := input_data [j..j-1];That works because Ada allows so-called "null slices" [ADA83, sec 4.1.2], and it treats this assignment as a no-op [ADA83, sec 5.2.1]. But it still causes an unnecessary packet to be sent, and it makes reassembly harder, because reassembly now has to be ready to handle empty packets, for which not even one bit of the reassembly map should be set. Even worse, as the procedure is currently written, that doesn't even happen, because the number of fragments is calculated incorrectly 😭
Here's an example to make it clearer. Say the total datagram length is 16 bytes and each fragment should carry 8 bytes. The statements above give number_of_fragments = (16 + 7)/8 = 2 and data_in_last_frag = 16 mod 8 = 0. Because those two values don't agree, instead of sending three fragments of lengths 8, 8, and 0, the procedure only sends two fragments, of lengths 8 and 0. The last eight octets never get sent at all 💔
To avoid all this, the specification should add the following statement right after computing data_in_last_frag:
if data_in_last_frag = 0 then
data_in_last_frag := data_per_fragment;
end if;This procedure also has a few smaller errors. Besides not accounting for packet header padding (listed in the next section), it fails to convert the header length from words (four octets) to octets in one step. The statement that calculates the total length of the non-tail fragments is:
to_SNP.dtgm.total_length := to_SNP.dtgm.header_length
+ data_per_fragment;Since header length is in words, this statement should read:
to_SNP.dtgm.total_length := to_SNP.dtgm.header_length * 4
+ data_per_fragment;This is apparently just a misprint, since the same calculation for the tail fragment is already done correctly 🎀
Problem 5: Errors in reassembly 🧩
The action procedure reassembly [MILS83a, sec 9.4.6.3.9], which the specification also calls reassemble elsewhere [MILS83a, sec 9.4.6.1.2, sec 9.4.6.1.3], puts an incoming fragment into the datagram being reassembled. This procedure has several relatively minor errors 🦋
In two places, a range is written to include one more member than it should. The first is where data from the fragment gets inserted into the datagram being reassembled:
state_vector.data [from_SNP.dtgm.fragment_offset*8 ..
from_SNP.dtgm.fragment_offset*8 + data_in_frag] :=
from_SNP.dtgm.data [0..data_in_frag-1];In this statement, the slice on the left has one more byte than the slice on the right. That causes a run-time exception to be raised [ADA83, sec 5.2.1]. The statement should read:
state_vector.data [from_SNP.dtgm.fragment_offset*8 ..
from_SNP.dtgm.fragment_offset*8 + data_in_frag - 1] :=
from_SNP.dtgm.data [0..data_in_frag-1];A similar problem shows up in the calculation of the range of bits in the reassembly map that matches the incoming fragment. This statement begins
Okay bestie, the loop header is where this gets messy 💀 Look at it:
for j in (from_SNP.dtgm.fragment_offset) ..
((from_SNP.dtgm.fragment_offset +
data_in_frag + 7)/8) loopThe parentheses are in the wrong spot 🙈 The function f(x) = (x + 7) / 8 is only supposed to run on data_in_frag, and this range also ends up with one extra member. The statement should read:
for j in (from_SNP.dtgm.fragment_offset) ..
(from_SNP.dtgm.fragment_offset +
(data_in_frag + 7)/8) - 1 loopBonus slay ✨ With this fix, the zero-length fragment from earlier gets handled too, because the loop doesn't run even once [ADA83, sS 5.5] 🦋
Next up is the header-saving part, and it's lowkey chaotic 😭 The relevant statement is:
state_vector.header := from_SNP.dtgm;This tries to shove the entire incoming fragment into a record that's only big enough for the header. In Ada that isn't a truncation, it's a run-time exception [ADA83, sec 5.2] 💀 The fix should be something like:
state_vector.header := from_SNP.dtgm.header;Here's the catch: you can't make that change without also defining the header portion of the datagram as a subrecord in [MILS83a, sec 9.4.4.6], and that would force a bunch of other statements to change too. For example, from_SNP.dtgm.fragment_offset would now have to be written as from_SNP.dtgm.header.fragment_offset. 🌸 Another option is to write the statement as a series of assignments, one for each field in the header, like this:
state_vector.header.version :=
from_SNP.dtgm.version;
state_vector.header.header_length :=
from_SNP.dtgm.header_length;
state_vector.header.type_of_service :=
from_SNP.dtgm.type_of_service;
-- etc.Also, this procedure will fail if any incoming fragment other than the tail fragment doesn't contain a multiple of eight characters. Implementors must be careful to check for this in the decision function SNP_params_valid [MILS83a, sec 9.4.6.2.7] 🫶
Heads up: this one's a real trap, so don't skip the check 🚨
Problem 6: Incorrect Data Length for Fragmented Datagrams 💅
The procedure reassembled_delivery [MILS83a, sec 9.4.6.3.10] doesn't hand the right data length to the upper-level protocol 😤 The culprit is this assignment:
to_ULP.length := state_vector.header.total_length
- state_vector.header.header_length * 4;Here's the tea ☕ Reassembly copies the header of the leading fragment into state_vector.header, as we talked about above. But the total_length field in that fragment only describes that one fragment, not the whole datagram. (This isn't super clear from its definition in [MILS83a, sec 9.3.4], but the fragment_and_send procedure [MILS83a, sec 9.4.6.3.7] makes sure that's how it works.)
So the length of the entire datagram can only be figured out from the length and offset of the tail fragment. That computation happens in the reassembly procedure [MILS83a, sec 9.4.6.3.9], and the result gets saved in state_vector.total_data_length (see above). Reassembly can't fill in state_vector.header.total_length at that point, though, because state_vector.header.header_length comes from the lead fragment, which might not have arrived yet 🥺
So reassembled_delivery needs to replace the statement above with:
to_ULP.length := state_vector.total_data_length;If this error isn't fixed, the upper-level protocol only gets told about as many octets as are in the lead fragment, and that's a whole lot of missing data 🧚
5. Implementation Difficulties of MIL Standard IP ✨
okay so beyond all the big problems we just went over, the MIL standard IP spec [MILS83a] has a bunch of features that make life hard for implementors 😭 these aren't technically errors in the spec. they're assumptions that never get said out loud, but you have to know about them anyway 🫶
5.1. Header Padding 🎀
in a few spots, the spec works out the length of a packet header without making room for padding. the padding matters because the spec requires [MILS83a, sec 9.3.14] that every header ends on a 32-bit boundary 💅
one spot where this shows up is the need_to_frag decision function [MILS83a, sec 9.4.6.2.5]. its job is deciding whether an outgoing datagram has to be fragmented. it's literally one statement:
if ((from_ULP.length + (number of bytes of option data)
+ 20) > maximum transmission unit of the local subnetwork
then return YES
else return NO;
end if;(also a tiny syntax slip: the first return statement is missing its semicolon [ADA83, sec 5.1, sec 5.3, sec 5.9] 🙈) to leave room for padding, the length of the outgoing datagram should be computed like this:
(((from_ULP.length + (number of bytes of option data) + 20)
+ 3)/4 * 4)another spot is the action procedure build_and_send [MILS83a, sec 9.4.6.3.2], which gets unfragmented datagrams ready to send. it works out the header_length field, which is measured in words (units of four octets) [MILS83a, sec 9.3.2], with this statement:
to_SNP.dtgm.header_length := 5 +
(number of bytes of option data)/4;to make room for padding, it should read:
to_SNP.dtgm.header_length :=
5 + ((number of bytes of option data)+3)/4;fragment_and_send [MILS83a, sec 9.4.6.3.7] has the exact same statement, since it prepares datagram fragments for sending, so it needs the same fix 🔥
fragment_and_send has this same issue in two more places. the first one works out how many octets go in each fragment:
data_per_fragment := maximum subnet transmission unit
- (20 + number of bytes of option data);to allow for padding, it should be:
data_per_fragment := maximum subnet transmission unit
- (((20 + number of bytes of option data)+3)/4*4);(okay but actually this one has to be changed even more, to:
data_per_fragment := (maximum subnet transmission unit
- (((20 + number of bytes of option data)+3)/4*4)/8*8;so it can do the job it was meant to do, for the reasons we already talked about above 🤓)
then there's the statement that works out the header length for each individual fragment:
to_SNP.dtgm.header_length := 5 +
(number of copy options octets/4);to allow for padding, it should become:
to_SNP.dtgm.header_length := 5 +
(number of copy options octets+3/4);✨ bestie, here's the easy version: all of these bugs can be fixed in one go if you just always read "number of bytes of option data," and phrases like it, as already including whatever padding is needed. 💖
5.2. Subnetworks with Small Transmission Sizes 🦋
when an outgoing datagram is too big to go out as one packet, it has to be fragmented. on some subnetworks, though, the most bytes you can send at once could be smaller than the IP packet header for that datagram. when that happens, the datagram can't be sent at all, not even fragmented 😵 that doesn't automatically mean the subnetwork can't send anything, because the header size can change a lot. when this problem comes up, IP should detect it. the right place to catch it is the can_frag function.
the can_frag decision function [MILS83a, sec 9.4.6.2.2] decides whether a particular outgoing datagram that's too long for one fragment is allowed to be fragmented. in the current spec, it's just this one statement:
if (from_ULP.dont_fragment = TRUE)
then return NO
else return YES
end if;(the return statements are also supposed to end in semicolons, which is another minor syntax error; see [ADA83, sec 5.1, sec 5.3, sec 5.9] 💀)
if the problem above happens, fragment_and_send ends up computing negative fragment sizes, and the results are unpredictable 😱 to prevent that, the subnetwork has to be able to send the datagram header plus at least one block (eight octets) of data. the can_frag function should be rewritten as:
if ((8 + ((number of bytes of option data)+3)/4*4 + 20)
> maximum transmission unit of the local subnetwork)
then return NO;
elsif (from_ULP.dont_fragment = TRUE)
then return NO
else return YES
end if;this logic is a lot like need_to_frag, which we covered above 💜
5.3. Subnetwork Interface 🌸
the spec does let the subnetwork report errors to IP [MILS83a, sec 6.3.6.2], but it never says what the IP entity should actually do when those errors happen. not cute 🙃
and the spec also says [MILS83a, sec 8.2.1.1] that the subnetwork should accept type-of-service indicators (precedence, reliability, delay, and throughput). on lots of local networks, that's going to be really hard to pull off 😩
5.4. ULP Errors 🍓
the IP spec [MILS83a, sec 9.4.6.3.6] says:
The format of error reports to a ULP is implementation dependent. However, included in the report should be a value indicating the type of error, and some information to identify the associated data or datagram.
the most natural way to give that second bit of info would be to hand the upper-level protocol the datagram identifier. that makes sense because the sending ULP is the one that supplies it in the first place [MILS83a, sec 9.3.5]. the problem is that the to_ULP data structure has no field for it [MILS83a, sec 9.4.4.3]. that's probably because the identifier is pointless for datagrams that come in from the subnetwork. implementors might feel they need to add that field to to_ULP anyway 🫶
5.5. Initialization of Data Structures 🌈
the reass_done decision function [MILS83a, sec 9.4.6.2.6] quietly assumes that the data structures inside each finite state machine get set to zero when the machine is created. specifically, this routine won't work unless state_vector.reassembly_map and state_vector.total_data_length are zeroed out like that 🧚 the spec never says this out loud, so implementors need to keep it in mind. there might be other initialization assumptions we haven't spotted yet ✨
5.6. Locally Defined Types 🔥
the procedures error_to_source [MILS83a, sec 9.4.6.3.5] and error_to_ULP [MILS83a, sec 9.4.6.3.6] define enumeration types inside comments. the first one has this comment:
error_param : (PARAM_PROBLEM, EXPIRED_TTL, PROTOCOL_UNREACH);and the second one has this:
error_param : (PARAM_PROBLEM, CAN'T_FRAGMENT, NET_UNREACH,
PROTOCOL_UNREACH, PORT_UNREACH);those enumerated values get used before they're ever defined [MILS83a, sec 9.4.6.1.1, sec 9.4.6.1.2, sec 9.4.6.1.3, et al.], so implementors will probably want to define some error types globally 👑
5.7. Miscellaneous Difficulties 💅
the spec is full of Ada syntax errors, and we showed some of them above. we only brought up syntax errors above when they came with other problems, though. one of the big syntax issues we haven't covered is that the spec often creates unnamed types by declaring records inside records. that's legal in Pascal, but not in Ada [ADA83, sec 3.7] 😭
another problem is that slice assignments often don't have the same number of elements on the left and right sides. that raises a run-time exception [ADA83, sec 5.2.1]. we already mentioned some of these, but there are others we didn't list 🙈
specifically, the procedure error_to_source [MILS83a, sec 9.4.6.3.5] has this statement:
to_SNP.dtgm.data [8..N+3] := from_SNP.dtgm.data [0..N-1];we think N+3 is a misprint for N+8, but even with that fixed, the left side still has one more byte than the right. implementors should check every slice assignment super carefully 🔍
6. An Implementation of MIL Standard IP 🎀
in our discussion above, we pointed out several serious problems with the Military Standard IP [MILS83a] spec. those have to be fixed before you can get a working implementation that conforms to this standard 🛠️ we did build a working C implementation of MIL Standard IP, once the problems we covered were fixed in the IP spec. what makes it special is that it was generated semi-automatically from the IP spec with the help of a protocol development system [BLUT82] [BLUT83] [SIDD83]. since it came straight from the IP spec with tools doing the work, it conforms to the IP standard better than any hand-coded IP implementation could 🤖✨
the problems in this paper with the current MIL Standard IP spec [MILS83a] come from an initial investigation of the protocol 🔎
NOTES
[1] Ada is a registered trademark of the U.S. Government - Ada Joint Program Office.
[2] d indicates a "don't care" condition.
ACKNOWLEDGEMENTS 💖
the author thanks Tom Blumer, Michael Breslin, Bob Pollack and Mark J. Vincenzes for lots of helpful discussions. thanks also to B. Simon and M. Bernstein for bringing the author's attention to a specification of the DoD Internet Protocol during 1981-82, when a detailed study of this protocol began. the author is also grateful to Jon Postel and Carl Sunshine for several informative discussions about DoD IP/TCP over the last few years 🌸
References ✨
okay bestie, this is the bibliography, and honestly it's giving research diary 📚🫶 every single source is listed below with all its details, so nobody gets left on read.
[ADA83] Military Standard Ada(R) Programming Language, United States Department of Defense, ANSI/MIL-STD-1815A-1983, 22 January 1983
[BLUT83] Blumer, T. P., and Sidhu, D. P., "Mechanical Verification and Automatic Implementation of Communication Protocols," to appear in IEEE Trans. Softw. Eng.
[BLUT82] Blumer, T. P., and Tenney, R. L., "A Formal Specification Technique and Implementation Method for Protocols," Computer Networks, Vol. 6, No. 3, July 1982, pp. 201-217.
[MILS83a] "Military Standard Internet Protocol," United States Department of Defense, MIL-STD-1777, 12 August 1983.
[MILS83b] "Military Standard Transmission Control Protocol," United States Department of Defense, MIL-STD-1778, 12 August 1983.
[POSJ81] Postel, J. (ed.), "DoD Standard Internet Protocol," Defense Advanced Research Projects Agency, Information Processing Techniques Office, RFC-791, September 1981.
[SDC82] DCEC Protocol Standardization Program: Protocol Specification Report, System Development Corporation, TM-7172/301/00, 29 March 1982
[SIDD83] Sidhu, D. P., and Blumer, T. P., "Verification of NBS Class 4 Transport Protocol," to appear in IEEE Trans. Comm.
[SIDD84] Sidhu, D. P., and Blumer, T. P., "Some Problems with the Specification of the Military Standard Transmission Control Protocol," in Protocol Specification, Testing and Verification IV, (ed.) Y. Yemini et al (1984).
That's the whole list, and honestly the MIL-STD-1777 and RFC-791 entries are the ones that matter most for this story 🧚💖
📦 where this page comes from
- ietf: rfc963 1985-11
- 💖 girlified by claude-haiku-5-5 on : a language model's rewrite of the original, under its terms