Bgp path attribute

Path Attributes:

     A variable-length sequence of path attributes is present in
     every UPDATE message, except for an UPDATE message that carries
     only the withdrawn routes.  Each path attribute is a triple
     <attribute type, attribute length, attribute value> of variable
     length.

     Attribute Type is a two-octet field that consists of the
     Attribute Flags octet, followed by the Attribute Type Code
     octet.

           0                   1
           0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5
           +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
           |  Attr. Flags  |Attr. Type Code|
           +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+

     The high-order bit (bit 0) of the Attribute Flags octet is the
     Optional bit.  It defines whether the attribute is optional (if
     set to 1) or well-known (if set to 0).

     The second high-order bit (bit 1) of the Attribute Flags octet
     is the Transitive bit.  It defines whether an optional
     attribute is transitive (if set to 1) or non-transitive (if set
     to 0).

     For well-known attributes, the Transitive bit MUST be set to 1.
     (See Section 5 for a discussion of transitive attributes.)

     The third high-order bit (bit 2) of the Attribute Flags octet
     is the Partial bit.  It defines whether the information
     contained in the optional transitive attribute is partial (if
     set to 1) or complete (if set to 0).  For well-known attributes
     and for optional non-transitive attributes, the Partial bit
     MUST be set to 0.

     The fourth high-order bit (bit 3) of the Attribute Flags octet
     is the Extended Length bit.  It defines whether the Attribute
     Length is one octet (if set to 0) or two octets (if set to 1).

     The lower-order four bits of the Attribute Flags octet are
     unused.  They MUST be zero when sent and MUST be ignored when
     received.

     The Attribute Type Code octet contains the Attribute Type Code.
     Currently defined Attribute Type Codes are discussed in Section
     5.

     If the Extended Length bit of the Attribute Flags octet is set
     to 0, the third octet of the Path Attribute contains the length
     of the attribute data in octets.

     If the Extended Length bit of the Attribute Flags octet is set
     to 1, the third and fourth octets of the path attribute contain
     the length of the attribute data in octets.

     The remaining octets of the Path Attribute represent the
     attribute value and are interpreted according to the Attribute
     Flags and the Attribute Type Code.  The supported Attribute
     Type Codes, and their attribute values and uses are as follows:

object path_attr = {
    type this

type this = struct { attr_flags: stream_pos, attr_flags: stream_pos, attr_len: stream_pos, attr_value: stream_pos }

     a) ORIGIN (Type Code 1):
        ORIGIN is a well-known mandatory attribute that defines the
        origin of the path information.  The data octet can assume
        the following values:
           Value      Meaning
           0         IGP - Network Layer Reachability Information
                        is interior to the originating AS
           1         EGP - Network Layer Reachability Information
                        learned via the EGP protocol \[RFC904\]
           2         INCOMPLETE - Network Layer Reachability
                        Information learned by some other means
        Usage of this attribute is defined in 5.1.1.

    object origin = {
        variant this of path_attr = struct {
            value: stream_pos
        }
    }

b) AS_PATH (Type Code 2): AS_PATH is a well-known mandatory attribute that is composed of a sequence of AS path segments. Each AS path segment is represented by a triple . The path segment type is a 1-octet length field with the following values defined: Value Segment Type 1 AS_SET: unordered set of ASes a route in the UPDATE message has traversed 2 AS_SEQUENCE: ordered set of ASes a route in the UPDATE message has traversed The path segment length is a 1-octet length field, containing the number of ASes (not the number of octets) in the path segment value field. The path segment value field contains one or more AS numbers, each encoded as a 2-octet length field. Usage of this attribute is defined in 5.1.2.

    object as_path = {
        object as_path_segment = {
            type this = struct {
                segment_type : segmenttype,
                segment_len  : autonomous_system.idx,
                segment_value: autonomous_system.arr
            }
            instance idx : unbounded_sequence
            instance arr : array(idx,this)
        }

        variant this of path_attr = struct {
            path: as_path_segment.arr
        }
    }

c) NEXT_HOP (Type Code 3): This is a well-known mandatory attribute that defines the (unicast) IP address of the router that SHOULD be used as the next hop to the destinations listed in the Network Layer Reachability Information field of the UPDATE message. Usage of this attribute is defined in 5.1.3.

    object next_hop = {
        variant this of path_attr = struct {
            next_hop: ip.addr
        }
    }

d) MULTI_EXIT_DISC (Type Code 4): This is an optional non-transitive attribute that is a four-octet unsigned integer. The value of this attribute MAY be used by a BGP speaker's Decision Process to discriminate among multiple entry points to a neighboring autonomous system. Usage of this attribute is defined in 5.1.4.

    object multi_exit_disc = {
        variant this of path_attr = struct {
            multi_exit_disc: stream_pos
        }
    }

e) LOCAL_PREF (Type Code 5): LOCAL_PREF is a well-known attribute that is a four-octet unsigned integer. A BGP speaker uses it to inform its other internal peers of the advertising speaker's degree of preference for an advertised route. Usage of this attribute is defined in 5.1.5.

    object local_pref = {
        variant this of path_attr = struct {
            local_pref: stream_pos
        }
    }

f) ATOMIC_AGGREGATE (Type Code 6) ATOMIC_AGGREGATE is a well-known discretionary attribute of length 0. Usage of this attribute is defined in 5.1.6.

    object atomic_aggregate = {
        variant this of path_attr = struct {
        }
    }

g) AGGREGATOR (Type Code 7) AGGREGATOR is an optional transitive attribute of length 6. The attribute contains the last AS number that formed the aggregate route (encoded as 2 octets), followed by the IP address of the BGP speaker that formed the aggregate route (encoded as 4 octets). This SHOULD be the same address as the one used for the BGP Identifier of the speaker. Usage of this attribute is defined in 5.1.7.

    object aggregator = {
        variant this of path_attr = struct {
            as_num: autonomous_system,
            ip_addr: ip.addr
        }
    }

    instance idx : unbounded_sequence
    instance arr : array(idx,this)
}


object path_attr = {
    ...
    action handle(f:this, src:bgp_id, dst:bgp_id) = {
        require false; # this generic action should never be called
    }
}

function queued_path_attr(C:bgp_id)     : path_attr.arr
function num_queued_path_attr(C:bgp_id) : path_attr.idx
function path_attr_size(C:bgp_id)       : stream_pos

function queued_segment_type(C:bgp_id,I:path_attr.as_path.as_path_segment.idx)      : segmenttype
function queued_segment_value(C:bgp_id,I:path_attr.as_path.as_path_segment.idx)     : autonomous_system.arr
function num_queued_segment_value(C:bgp_id,I:path_attr.as_path.as_path_segment.idx) : autonomous_system.idx
function num_queued_as_path(C:bgp_id)                                               : path_attr.as_path.as_path_segment.idx

ORIGIN is a well-known mandatory attribute that defines the origin of the path information.

relation origin_present(C:bgp_id)

object path_attr = {
    ...
    object origin = {
        ...
        action handle(f:path_attr.origin, src:bgp_id, dst:bgp_id)

        around handle {

TODO use an action to make this general require src = bgp_ivy_instance.bgpid; require dst = bgp_impl_instance.bgpid;

            require open_message_recv(src) & open_message_recv(dst);
            require ~origin_present(src);
            require header_type = bgp_message_type.update_mess;
            ...
            path_attr_size(src) := path_attr_size(src) + 1 + 1 + 1 + 1;
            origin_present(src) := true;
            call enqueue_path_attr(src,f);
        }
    }
}

action as_idx_to_stream_pos(c:autonomous_system.idx) returns(res:stream_pos) = {
    <<<
    res = c;
    >>>
}

object path_attr = {
    ...
    object as_path = {
        ...
        action handle(f:path_attr.as_path, src:bgp_id, dst:bgp_id)

        around handle {
            var idx : path_attr.as_path.as_path_segment.idx := 0;
            require open_message_recv(src) & open_message_recv(dst);
            require f.path.end > 0; # & f.path.end = num_queued_as_path(src);
            require header_type = bgp_message_type.update_mess;
            while idx < f.path.end {
                var aspath := f.path.value(idx);
                if ~_generating {
                    queued_segment_type(src,idx) := aspath.segment_type;
                    num_queued_segment_value(src,idx) := aspath.segment_value.end;
                    queued_segment_value(src,idx) := aspath.segment_value;
                };
                require queued_segment_type(src,idx) = 1 | queued_segment_type(src,idx) = 2;
                require aspath.segment_type  = queued_segment_type(src,idx);
                require aspath.segment_len   = num_queued_segment_value(src,idx);
                require aspath.segment_value = queued_segment_value(src,idx);
                path_attr_size(src) := path_attr_size(src) + 1 + 2 * as_idx_to_stream_pos(aspath.segment_len);
                idx := idx.next;
            };
            ...
            path_attr_size(src) := path_attr_size(src) + 1 + 1 + 2 + 1;
            var jdx : path_attr.as_path.as_path_segment.idx := 0;
            while jdx < num_queued_as_path(src) {
                queued_segment_type(src,jdx) := 0;
                num_queued_segment_value(src,jdx) := 0;
                queued_segment_value(src,jdx) := autonomous_system.arr.empty;
                jdx := jdx.next;
            };
            num_queued_as_path(src) := 0;
            call enqueue_path_attr(src,f);
        }
    }
}

object path_attr = {
    ...
    object next_hop = {
        ...
        action handle(f:path_attr.next_hop, src:bgp_id, dst:bgp_id)

        around handle {
            require open_message_recv(src) & open_message_recv(dst);
            ...
            path_attr_size(src) := path_attr_size(src) + 1 + 1 + 1 + 4;
            call enqueue_path_attr(src,f);
        }
    }
}

object path_attr = {
    ...
    object multi_exit_disc = {
        ...
        action handle(f:path_attr.multi_exit_disc, src:bgp_id, dst:bgp_id)

        around handle {
            require open_message_recv(src) & open_message_recv(dst);
            ...
            path_attr_size(src) := path_attr_size(src) + 1 + 1 + 1 + 4;
            call enqueue_path_attr(src,f);
        }
    }
}

object path_attr = {
    ...
    object local_pref = {
        ...
        action handle(f:path_attr.local_pref, src:bgp_id, dst:bgp_id)

        around handle {
            require open_message_recv(src) & open_message_recv(dst);
            ...
            path_attr_size(src) := path_attr_size(src) + 1 + 1 + 1 + 4;
            call enqueue_path_attr(src,f);
        }
    }
}

object path_attr = {
    ...
    object atomic_aggregate = {
        ...
        action handle(f:path_attr.atomic_aggregate, src:bgp_id, dst:bgp_id)

        around handle {
            require open_message_recv(src) & open_message_recv(dst);
            ...
            path_attr_size(src) := path_attr_size(src) + 2 +1 + 1 + 1 +  4;
            call enqueue_path_attr(src,f);
        }
    }
}

action enqueue_path_attr(src:bgp_id, f:path_attr) = {
    queued_path_attr(src)     := queued_path_attr(src).append(f);
    num_queued_path_attr(src) := queued_path_attr(src).end;
    if ~(f isa path_attr.origin){ #& ~(f isa frame.padding){
        origin_present(src) := true;
    };
}