TECHNICAL REPORT 04-02

Correctness Proof of the SBT method

Yutaka Sugawara and Kei Hiraki

October 20, 2004

Department of Information Science
Faculty of Science, University of Tokyo

7–3–1 Hongo, Bunkyo-Ku Tokyo, 113 JapanTECHNICAL REPORT 04-02
TITLE
Correctness Proof of the SBT method

AUTHORS
Yutaka Sugawara, Mary Inaba, and Kei Hiraki
KEY WORDS AND PHRASES
string matching, FPGA, SBT, correctness proof
ABSTRACTIn this paper, we prove the correctness of the SBT method, which we proposed in a previous paper[1]. SBT is a string matching method optimized for high-speed multi-stream packet scanning on
FPGA. The SBT method is capable of lightweight switching between TCP streams, and enables
easy implementation of multi-stream scanners. In addition, we achieved over 10Gbps string matching bandwidth using a Xilinx XC2V6000 FPGA. In this paper, we present a correctness proof of the
SBT method, which we could not presented in the previous paper [1] due to the space limitation.

REPORT DATE
October 20, 2004

WRITTEN LANGUAGE
EnglishTOTAL NO. OF PAGES
11

NO. OF REFERENCES
12ANY OTHER IDENTIFYING INFORMATION OF THIS REPORTDISTRIBUTION STATEMENT
This technical report is available ONLY via anonymous
ftp.is.s.u-tokyo.ac.jp (directory /pub/tech-reports).
SUPPLEMENTARY NOTESDEPARTMENT OF INFORMATION SCIENCE
Faculty of Science, University of Tokyo
7-3-1 Hongo, Bunkyo-ku, Tokyo 113, Japan

FTP

from

Correctness Proof of the SBT method
Yutaka Sugawara, Mary Inaba, and Kei Hiraki

1

Introduction

Recent technology has realized fast networks such as 10Gbit Ethernet and OC-768. To takeadvantage of such high-speed networks, it is necessary to accelerate network applications. Partof the applications requires intensive packet payload scanning. For example, in network intrusion
detection systems (NIDS), payload scanning to ﬁnd suspicious patterns occupies the major partof the computation time[2]. Other examples include Content-based billing, SPAM ﬁltering,and HTTP request distribution. To accelerate them, fast string matching is necessary. In thematching, a set of byte strings (rules) is statically given, and occurrences of the strings in input
packet streams are checked.
When matching speed alone is important, hardware implementation is better than software
implementation. However, it is also necessary to update pattern rules. For example, in NIDS,
rules are frequently updated to cope with the patterns found in new intrusion methods. Therefore, we cannot hard-wire rules because the rule update is impossible without replacing the hardware. FPGA based implementation is a solution for string matching in hardware while allowing
the rules to be updated. When FPGAs are used, the rules can be changed by reconﬁguration.
There are studies of string matching using FPGAs such as comparator based methods[3][4],CAM based methods[5], non-deterministic automaton(NFA) based methods[6][7][8], deterministic ﬁnite automaton(DFA) based methods[9], Bloom Filter based methods[10], and KnuthMoris-Pratt(KMP) algorithm based methods[11]. They enabled high-speed string matching
while allowing the rules to be changed. For a high throughput under a limited clock speed, it
is important to process multiple input characters at once[3][4][8].
In TCP, a communication data stream is split into packets. Therefore, a target pattern may
span multiple packets. Such fragmented pattern cannot be discovered by a per-packet scan.
This is a serious problem in applications such as NIDS that require a complete scan. To avoid
the problem, it is necessary to scan TCP streams. However, existing FPGA based methods
cannot be used for scanning multiple streams because of the diﬃculty in switching between
streams.
In [1], we proposed a string matching method called suﬃx based traversing (SBT). SBT
is an extension of the Aho-Corasick algorithm[12], which uses table lookup in state transition.
Since a small number of state bits are used in the SBT method, lightweight stream switchingis enabled. The main points of extension for SBT are (1)processing multiple input bytes atonce, and (2)table size reduction. When the Aho-Corasick algorithm is naively extended toprocess multiple bytes, a large lookup table is necessary. We solved this problem by reducing
the number of table input patterns. As a result, the large table is converted into smaller tables
and over 10Gbps scanning is enabled.
In the previous paper [1], we did not present the correctness proof of the SBT method
because of the space limitation, though it is mandatory for a complete algorithm description.
In this paper, we present the correctness proof.
In Section 2 we describe the SBT method. Section 4 presents the correctness proof of the
SBT method. We conclude this paper in Section 5.
1

~(a|b)

~a

~a

a

a

’’

a ’a’ a ’aa’ a ’aaa’ b ’aaab’ b ’aaabb’babb~(a|b)aoutput function’ab’ b ’abb’

node
’ab’
’abb’
’aaab’’aaabb’others~arules = { ’aaabb’, ’abb’, ’ab’ }match output
’ab’
’abb’
’ab’
’abb’, ’aaabb’
none

Figure 1: An example FSM of Aho-Corasick algorithm

2Outline of SBT Method

2.1

Aho-Corasick Algorithm

In Aho-Corasick algorithm[12], a trie is built that contains all the rule strings. Then, the string
matching is performed using a state machine whose state is a node position of the trie. The
initial state is the root node of the trie. Each time a character of the string is input, the statetransits from the current node to the next node through the transition edge corresponds to the
input character1 . The current state node corresponds to the longest suﬃx of the input string
up to this time.
The output function is deﬁned for each state node. The output function indicates what
rule strings are matched when each state node is reached. Note that the output format of thematch results depends on the application2 . We must change the output function according tothe output format. In this paper, we discuss only the state transition, and we do not discuss
the matching result output. Figure 1 is an example FSM used in Aho-Corasick algorithm.

2.2

Optimization of FSM Based Method

In the description of this paper, all the strings consist of 1 octet (8 bit) characters. When string
matching is performed using an FSM based method with state transition table lookup, we must
optimize the implementation in the following respects:• Parallel processing of multiple input characters.
• Memory size reduction of the state transition tables.
The former is important to realize high matching throughput under a limited clock speed.
In an FSM based method, when the state transition table lookup is performed in an sequential
manner, it is impossible to process multiple characters in parallel. To process multiple charactersin parallel, it is necessary to change the implementation of state lookup mechanism.
The later is necessary for implementing the state transition tables using FPGA on-chip
memories. Since oﬀ-chip memories are slower than oﬀ-chip ones, high performance cannot
be achieved by oﬀ-chip memory implementations. In addition, when multiple characters areprocessed in parallel, oﬀ-chip implementations are very diﬃcult because many independent
memory chips are necessary.
1
In Aho-Corasick algorithm, it is possible not to enumerate all the transition edges by using the failure
function. However, we use an implementation without the failure function because it is suitable for hardware
implementation since the processing amount of each cycle is constant.
2
For example, in an application, just the longest matching rule string is output.

2

Aho-Corasick:state0astate1bstate2cstate3

Idea of SBT:astate1babcd

state2state4estate5flook-aheadabcdstate0dcstate3state6gstate7estate5fstate8look-aheadefghstate4hstate6gstate7state8efgh

state0state4aestate8state12state16

state1state5state9state13bf

state2state6state10cgstate3time

Parallelism

state7

Figure 2: Parallel processing of multiple characters using look-ahead tables
abcd

abstate0astate1state2cstate3abcdefghstate8state9state10estate5

ijkl

ij
i

ef

state4kgstate7mn
mstate11state6state12state13state14ostate15

ijklmnop
8C look-aheadstate

1C look-ahead

4C look-ahead2C look-ahead1C look-ahead
1C look-ahead

2C look-ahead1C look-ahead

Figure 3: Tree-wise state look-ahead

2.3

Parallel Processing of Characters using Look-ahead Tables

In SBT method, state look-ahead table is used to get a state after a speciﬁed numberof characters. We call a state look-ahead table that tells a state after n characters as ncharacters look-ahead table. The n-characters look-ahead table receives the current state andthe succeeding n characters, and returns the state after the n characters3 . Using the look-ahead
tables, multiple state transitions can be calculated in parallel. For example, in Figure 2, 4 statetransitions are calculated in parallel using a 4-characters look-ahead table.
In an implementation like Figure 2, the calculation latency is O(w) when w characters
are processed in parallel. To reduce the latency to O(log w), a tree-wise state look-ahead is
performed in SBT method, as shown in Figure 3. Though the w can be an positive integer thatis not a power of 2, in this paper, we limit the w to a power of 2 for simplicity.

2.4

Memory Usage Reduction

2.4.1

Input pattern classiﬁcation

One naive implementation of n-characters state look-ahead table is to lookup a table of 2b+8w
entries using a b + 8w bits value that is the concatenation of the current state ID and the w
3

1-characters look-ahead table is state transition table itself.

32-characters state look-ahead table
longest suffix
ID calculation

→
→
→
→
→

’aa’ 0’ab’ 1’bb’ 2
input character 2’*a’ 3’**’ 4
input character 1

suffixID

current state

suffix ID

state
’’
’a’
’aa’
’ab’
’aaa’
’abb’
’aaab’’aaabb’

0
3 4
2
1
aa
a *
bb
ab
’aa’ ’ab’’a’ ’’’’’aaa’ ’ab’
’abb’ ’a’ ’’’aaa’ ’aaab’ ’abb’ ’a’ ’’’aa’ ’ab’’a’ ’’’’’aaa’ ’aaab’ ’aaabb’ ’a’ ’’’aa’ ’ab’’a’ ’’’’’aa’ ’ab’’a’ ’’’’’aa’ ’ab’’a’ ’’’’

Figure 4: State look-ahead table lookup using suﬃx pattern ID* Upper rule has higher priority
0(’aa’) x 0(’aa’)
input character 1 ’aa’ 0
suffix0(’aa’) x 1(’ab’)’ab’ 1ID
0(’aa’) x 2(’bb’)’bb’ 23(’*a’) x 0(’aa’)
input character 2 ’*a’ 33(’*a’) x 2(’bb’)’**’ 4all x 0(’aa’)
input character 3 ’aa’ 0
suffix
all x 1(’ab’)’ab’ 1ID
all x 2(’bb’)’bb’ 2all x 3(’*a’)
input character 4 ’*a’ 3
all x 4(’**’)’**’ 4

Length 2
suffix ID combination table2(’*aaa’)0(’aaab’)1(’aabb’)2(’*aaa’)3(’*abb’)4(’**aa’)5(’**ab’)7(’****’)
6(’***a’)7(’****’)

suffixID

Length 4
suffix ID combination table

Figure 5: Hierarchical calculation of suﬃx ID
input characters (b is the bit width of the state ID). However, the drawback of this method isthat the memory usage increases rapidly as the w increases. For example, when w = 8, thenumber of the table entries is more than 264 . Therefore, the implementation is diﬃcult.
However, lookup tables have a redundancy that it returns a non-initial state only when
the input characters have limited suﬃx patterns. We can reduce the memory size using theredundancy. For example, in the 2-characters lookup table of the rules shown in Figure 1,
though the total number of 2-character input patterns is 216 , the table returns a non-initialstate only when a suﬃx of the input character is ’aa’，’ab’，’bb’， or ’a’.
Therefore, we can reduce the size of the lookup tables by classifying the input character
patterns based on its suﬃx pattern and looking up the look-ahead table using the suﬃx ID,
as shown in Figure 4. In the example of Figure 4, the number of the columns is reduced from
216 to 5.
The suﬃx ID calculation is performed in an hierarchical manner using suﬃx ID combination tables, as shown in Figure 5. First, IDs are assigned to the necessary suﬃx patternsof length k strings for k = 2, 4, 8, . . . , w. A k-characters suﬃx ID combination table receives
two suﬃx IDs of length k/2 strings, and returns the suﬃx ID of the length k string that is theconcatenation of the two k/2 length strings. Using the hierarchical suﬃx ID calculation, thetable size is reduced.
2.4.2

Table size reduction using indirect pointers

Even when the number of columns of the look-ahead tables are reduced using suﬃx IDs, thelook-ahead tables have a redundancy that each row has a value that appears frequently. For
example, in Figure 4, ’aa’ appears frequently in the column 0(’aa’), and ’’ appears frequently
in the column 2(’bb’). The suﬃx ID combination tables have a similar redundancy. We canreduce the table size using the redundancy, as shown in Figure 6. First, the default value

4column
row
0

0

1

A

2 3

1
2

row pointer
table

B

C

D

3

row IDE

default

A

F G H

B
C

D
E

A C B E D

I

column ID

→0
→
→1
→1
0→F
1→G
2→H
3→I
0
1
2
3

row elemnt table(row ID, value)→ (0,A)→ (2,C) row ID→ (0,B)→ (3,E) value→ (2,D) 1 output
=?

don’t
care

+

0
1
2
3
4

0
defualt
value table

Figure 6: Table size reduction using row pointerstable is built that holds the value that appears most frequently for each row. Next, the original
table is decomposed into rows, and the column elements that diﬀer from the default table values
are stored in the row element table. The owner row ID is stored for each element in the row
element table. Finally, the row pointer table is built that holds the starting index of each row
in the row element table. Each empty element of the upside-left table in Figure 6 is identicalto the default value of the column.
In a table lookup, the row pointer table is looked up using the row index. Simultaneously,
the default value table is looked up using the column ID. Then the column ID is added to therow pointer to make the index of the row element table. The row element table is looked up
using the index. The returned row ID is compared with the input row ID. When they matched,
the value in the row element table is output. Otherwise, since the value of the row element
table is invalid, the value of the default value table is output.

3

Formal Algorithm Description of SBT Method

We denote the w input bytes as a w bytes string pin . Let P be the set consisting of all the rulestrings pi . The character indices of strings start from 0. The length of the string p is written as|p|. We write the concatenation of strings p and p as p :: p . substr(p, i, j) is the j characters
substring of p starting from position i, and prefix(p, k) = substr(p, 0, k). We write p  p
when the string p is p itself or a suﬃx of p . IN(X, p) is the IN of the longest string p in X
which satisﬁes p  p.
Variables and Tables T = {p | p  pi (pi ∈ P )} .
all the byte characterswhen k = 1
Ik = 
(substr(p,j,k)∪
prefix(p,l))
whenk = 2, 4, 8, · · · , wiii,j,l(l<k)

for k = 2, 4, 8, · · · , w and p, p ∈ Ik/2 ,IN(Ik , p )when |p | < k/2

Ck (IN(Ik/2 , p), IN(Ik/2 , p )) =
IN(Ik , p :: p ) when |p | = k/2
for k = 1, 
2, 4 · · · , w and i = 0, k, 2k, · · · , w − k and p ∈ Ik and s ∈ T ,IN(I1 , substr(pin , i, 1))
when k = 1
m(k, i) =i+
k/2))
when k ≥ 2
Ck (m(k/2, i), m(k/2,IN(T, p)when |p| < k
N Sk (IN(T, s), IN(Ik , p)) =IN(T, s :: p)) when |p| = k
T is the nodes of the rule string trie. Ik is the input suﬃxes for N Sk table. Table Ck tells the IN of the longest suﬃx of given 2 suﬃxes’ concatenation. m(k, i) is
IN(Ik , substr(pin , i, k)), the IN of the longest suﬃx of a portion of pin . Table N Sk tells
the state change after k characters.

5pin[3]C2 m(2,2)C4 m(4,0)

NS4

S

NS1

pin[2]
pin[1]r(2)NS2

C2 m(2,0)NS1

pin[0]

r(3)
r(1)
r(0)

suffix calculator state manager<=u? mt(3)<=u? mt(2)
match
<=u?
mt(1) flags
<=u?
mt(0)
match numbers

Figure 7: Structure of the pattern matcher when w = 4
Static Preparation Make T , Ik from given P and assign INs. The INs of the elements in I1
are their character codes. In the IN assignment of T , the elements which match some pi(i.e. {p | p ∈ T and pi  p for some pi }) are numbered ﬁrst, and then the other elements
are numbered, in increasing order. Let u be the maximum IN of the elements in T whichmatch some pi . Then, calculate lookup tables Ck and N Sk .
Input In each cycle, w characters of stream data are input. Let pin (t) be the w input charactersof the t-th clock cycle.
Output Let qi = pin (0) :: · · · :: pin (t − 1) :: prefix(pin (t), i). In each cycle, for each qi , thefollowing are output: (1) r(i) : IN(T, qi ), i.e. the IN of the longest string in T that matchesqi , and (2) mt(i) : A match flag which indicates whether qi matches some pj .
Algorithm Procedure Let S be a state variable which holds IN(T, pin (0) :: · · · :: pin (t − 1)).
In each clock, do following using lookup tables:
1. Calculate each m(k, i) from the input pin (t).
2. Calculate r(i) (i = 0, ..., w − 1) recursively: r(0) = S,
k = 1, 2, 4, · · · , wk(2l + 1) < wr(k(2l + 1)) = N Sk (r(2kl), m(k, 2kl))
3. mt(i) = true if r(i) ≤ u. Otherwise, mt(i) = f alse.
4. Assign the next state N Sw (S, m(w, 0)) to S

4

Correctness Proof

In the following description, p, p , q, q  , r, s are strings, and X is a set of strings.
Deﬁnition 1
LS(X, p) is the longest string p in X which satisﬁes p  p.
Following corollaries are immediately derived from the deﬁnition of the LS function.
Corollary 1p  p → |p | ≤ |p|Corollary 2LS(X, p) ∈ X
Corollary 3
p  q∧q r →p  r

6

Corollary 4
p  q ↔ p :: r  q :: rCorollary 5LS(X, p)  p
Proposition 1p  p ∧ p  p → p = pProofFrom Corollary 1, |p| = |p | is derived. By the deﬁnition of the  operator, |p| = |p | is satisﬁed
only when p = p
Proposition 2p  p , p ∈ X → LS(X, p)  p
Proof
Since p  p , LS(X, p) is p itself or a string that contains p as a suﬃx. Therefore, LS(X, p)  p
Proposition 3
p ∈ X → LS(X, p) = p
Proof
By putting p = p in Proposition 3, LS(X, p)  p is derived. By Corollary 5, LS(X, p)  p
stands. Therefore, using Proposition 1, LS(X, p) = p is derived
Corollary 6LS(X, LS(X, p)) = LS(X, p)
Proof
Because of Corollary 2, LS(X, p) ∈ X. Therefore, from Proposition 3, LS(X, LS(X, p)) =LS(X, p) is derived
Proposition 4p  p → LS(X, p)  LS(X, p )Proof
By Corollary 5, p  LS(X, p ) stands. Therefore, from Corollary 3, p  LS(X, p ) is derived.
By Corollary 2, LS(X, p ) ∈ X stands. Therefore, from Proposition 2, LS(X, p)  LS(X, p ) is
derived
Proposition 5p  p  LS(X, p) → LS(X, p ) = LS(X, p)
Proof
When p  p  LS(X, p), using Proposition 4, LS(X, p)  LS(X, p )  LS(X, LS(X, p)) is
derived. Therefore, by Corollary 6, LS(X, p)  LS(X, p )  LS(X, p) stands. Therefore, from
Proposition 1, LS(X, p) = LS(X, p ) is derived.
Lemma 1For k = 2, 4, 8, · · · , w,
Ck (IN(Ik/2 , p), IN(Ik/2 , p )) = IN(Ik , p :: p ) where |p| = |p | = k/2.
7

Proof
Let q = LS(Ik/2 , p), q  = LS(Ik/2 , p ), and r = LS(Ik , p :: p ). By deﬁnition of IN, IN(Ik/2 , p) =IN(Ik/2 , q) and IN(Ik/2 , p ) = IN(Ik/2 , q  ).
• When |r| ≥ k/2
r  p stands. Therefore we can put r = rp :: p , where rp = prefix(r, |r| − k/2).
Because of the deﬁnition of Ik and Ik/2 , rp , p ∈ Ik/2 stands. Therefore, from Proposition
3, q  = LS(Ik/2 , p ) = p is derived.
Since p  rp and rp ∈ Ik/2 , from Proposition 2, q = LS(Ik/2 , p)  rp is derived. Therefore,
by Corollary 4, q :: q  = q :: p  rp :: p = r = LS(Ik , p :: p ). Since p  q, by Corollary 4,
p :: p = p :: q   q :: q  stands. Therefore, from Proposition 5, LS(Ik , p :: p ) = LS(Ik , q ::q  ) is derived.
Therefore, since |q  | = |p | = k/2, Ck (IN(Ik/2 , p), IN(Ik/2 , p )) = Ck (IN(Ik/2 , q), IN(Ik/2 , q  )) =IN(Ik , q :: q  ) = IN(Ik , p :: p ).
• When |r| < k/2p  r stands.
– When |q  | = k/2
Since q  = p , 4, p :: p = p :: q   q :: q  stands. Furthermore, q :: q  > q  =p > r = LS(Ik , p :: p ). Therefore, by Corollary 3, q :: q  > LS(Ik , p :: p ) stands.
Therefore, from Proposition 5, LS(Ik , q :: q  ) = LS(Ik , p :: p ) is derived. Since|q  | = k/2, Ck (IN(Ik/2 , p), IN(Ik/2 , p )) = Ck (IN(Ik/2 , q), IN(Ik/2 , q  )) = IN(Ik , q ::q  ) = IN(Ik , p :: p ).
– When |q  | < k/2
By the deﬁnition of Ik and Ik/2 , r ∈ Ik/2 stands. Since p  r, by Proposition 2,
q  = LS(Ik/2 , p )  r = LS(Ik , p :: p ) stands. Furthermore, since p :: p  p  q  , p ::p  q  stands. Therefore, by Proposition 5, LS(Ik , q) = LS(Ik , p :: p ) stands. Since|q  | < k/2, Ck (IN(Ik/2 , p), IN(Ik/2 , p )) = Ck (IN(Ik/2 , q), IN(Ik/2 , q  )) = IN(Ik , q  ) =IN(Ik , p :: p )Lemma 2For k = 1, 2, 4, · · · , w,
N Sk (IN(T, s), IN(Ik , p)) = IN(T, s :: p).
Proof
The Lemma is proved in a way similar to Lemma 1.
Lemma 3For k = 1, 2, 4, · · · , w and i = 0, k, 2k, · · · , w − k, m(k, i) = IN(Ik , substr(pin , i, k)).
Proof
We prove the Lemma by a derivation on k.
• When k = 1
By the deﬁnition, m(k, i) = m(1, i) = IN(I1 , substr(pin , i, 1). Therefore, the Lemma
stands.
• When the Lemma stands for k = k /2 (k ≥ 2)
By the assumption of the derivation, m(k, i) = Ck (m(k /2, i), m(k /2, i+k /2)) = Ck (IN(Ik /2 , substr(pin , i,k /2, k /2))). Therefore, by Lemma 1, m(k, i) = IN(Ik , substr(pin , i, k /2) :: substr(pin , i+8k /2, k /2)) = IN(Ik , substr(pin , i, k ) stands. Therefore, the Lemma also stands fork = k .
Lemma 4In t-th clock cycle, S = IN(T, pin (0) :: pin (1) :: · · · :: pin (t − 1)).
Proof
We prove the Lemma by a derivation on t
• When t = 0
The Lemma stands since the S is initialized to IN(T,  ).
• When the Lemma stands for t = t − 1
By the assumption of the derivation, in (t − 1)-th clock cycle, S = IN(T, pin (0) :: pin (1) ::· · · :: pin (t − 2)). Since m(w, 0) = IN(Iw , pin ) stands by Lemma 3, in t -th clock cycle,
S = N Sw (IN(T, pin (0) :: pin (1) :: · · · :: pin (t − 2)), IN(Iw , pin (t − 1))). Therefore, byLemma 2, S = IN(T, pin (0) :: pin (1) :: · · · :: pin (t − 1)). Thus, the Lemma also stands
when t = tFinally, we show that the SBT method always outputs correct pattern IDs by proving thefollowing theorem.
Theorem 1
For i = 1, 2, 3, · · · , w, (A) r(i) is uniquely deﬁned, and (B) In t-th clock cycle, r(i) = IN(T, pin (0) ::pin (1) :: · · · :: pin (t − 1) :: substr(pin (t), 0, i)).
Proof
For i = 0, r(0) is uniquely deﬁned as r(0) = S = IN(T, pin (0) :: pin (1) :: · · · :: pin (t − 1) ::substr(pin (t), 0, 0)). Therefore, both (A) and (B) stand.
For other i, we prove the theorem by proving that the following lemma stands for all j(0 ≤j ≤ log w − 1) by a derivation on j.
(A) and (B) stands for all the integers i that satisﬁes num2s(i) = j, where the num2sfunction returns the number of 2’s the argument integer has as the primary factors.
Since 2l + 1 is an odd number in the deﬁnition of r(i), i = k(2l + 1) stands only when k =2num2s(i) . Since the k is uniquely determined, the value of the l is also uniquely determined(l =(i/k − 1)/2). Therefore, the combination of k and l that satisﬁes i = k(2l + 1) is unique.
Therefore, r(i) is deﬁned at most one time for each i. Thus, we can prove (A) by simply
showing that each r(i) is really deﬁned.
• When j = log w − 1
Only i = w/2 satisﬁes num2s(i) = j. For this i, i = k(2l + 1) is satisﬁed whenk = w/2 and l = 0. Therefore, r(w/2) = N Sw/2 (r(2 ∗ w/2 ∗ 0), m(w/2, 2 ∗ w/2 ∗ 0)) =N Sw/2 (r(0), m(w/2)) = N Sw/2 (S, IN(Iw/2 , substr(pin (t), 0, w/2)) = N Sw/2 (IN(T, pin (0) ::pin (1) :: · · · :: pin (t − 1)), IN(Iw/2 , substr(pin (t), 0, w/2)) = IN(T, pin (0) :: pin (1) :: · · · ::pin (t − 1)) :: substr(pin (t), 0, w/2)). Thus (B) is satisﬁed. Furthermore, since r(0) is
uniquely deﬁned, (A) is satisﬁed.
• When (A) and (B) is satisﬁed for j > j 
For each i such that num2s(i) = j  , in the deﬁnition of r(i), i = k(2l + 1) stands only
when k = 2j . Since num2s(2kl) = num2s(2 · 2j l) = num2s(2j +1 l) ≥ j  + 1, by the9assumption of the derivation, (A) and (B) stands for i = 2kl. Therefore, for each i suchthat num2s(i) = j  ,r(i) = r(k(2l + 1))= N Sk (r(2kl), m(k, 2kl))= N Sk (IN(T, pin (0) :: pin (1) :: · · ·:: pin (t − 1) :: substr(pin (t), 0, 2kl)), IN(Ik , substr(pin (t), 2kl, k)))= IN(T, pin (0) :: pin (1) :: · · ·:: pin (t − 1) :: substr(pin (t), 0, 2kl) :: substr(pin (t), 2kl, k))= IN(T, pin (0) :: pin (1) :: · · ·:: pin (t − 1) :: substr(pin (t), 0, k(2l + 1)))stands. Therefore, both (A) and (B) is satisﬁed for j = j  .

5Concluding Remarks

In this paper, we have presented the correctness proof of SBT method [1]. Therefore, thealgorithm description of SBT method is now complete. However, we must further analyze
the SBT method in respects including the worst case memory usage and the optimal packing
method of row elements into a row element table. These aspects are important for a practicaluse of SBT method. We will present the analysis as our future work.

Acknowledgements
This research is partially supported by the Special Coordination Fund for Promoting Science andTechnology, CREST project of Japan Science and Technology Corporation, and 21st century
COE project of Japan Society for the Promotion of Science.

References[1] Y. Sugawara, M. Inaba, K. Hiraki, “Over 10gbps string matching mechanism for multistream packet scanning systems,” in Proc. of 14th Intl. Conf. on Field Programmable Logic
and Applica tions(FPL ’04), August 2004.
[2] C. J. Coit, S. Staniford, J. McAlerney, “Towards Faster String Matching for Intrusion Detection or Exceeding the Speed of Snort,” in DISCEXII, DARPA Information Survivability
conference and Exposition, 2001.
[3] Y. H. Cho, S. Navab, W. H. Mangione-Smith, “Specialized Hardware for Deep Network
Packet Filtering,” in Proc. of 12th Intl. Conf. on Field Programmable Logic and Applications(FPL ’02), September 2002.
[4] I. Sourdis, D. Pnevmatikatos, “Fast, Large-Scale String Match for a 10Gbps FPGA-based
Network Intrusion Detection System,” in Proc. of 13th Intl. Conf. on Field Programmable
Logic and Applications(FPL ’03), September 2003.

10

[5] M. Gokhale, D. Dubois, A. Dubois, M. Boorman, S. Poole, V. Hogsett, “Granidt: Towards
Gigabit Rate Network Intrusion Detection Technology,” in Proc. of 12th Intl. Conf. on
Field Programmable Logic and Applications(FPL ’02), September 2002.
[6] R. Sidhu, V. K. Prasanna, “Fast regular expression matching using fpgas,” in Proc. of 9thIEEE Symp. on Field-Programmable Custom Computing Machines (FCCM’01), April –May 2001.
[7] B. L. Hutchings, R. Franklin, D. Carver, “Assisting network intrusion detection with reconﬁgurable hardware,” in Proc. of 10 th Annual IEEE Symp. on Field-Programmable Custom
Computing Machines (FCCM’02), pp. 111–120, September 2002.
[8] C. Clark, D. Schimmel, “Scalable pattern matching for high speed networks,” in Proc. of
12th IEEE Symp. on Field-Programmable Custom Computing Machines (FCCM’04), April
2004.
[9] J. Moscola, J. Lockwood, R. P. Loui, M. Pachos, “Implementation of a contentscanning module for an internet ﬁrewall,” in Proc. of 11th Annual IEEE Symp. on FieldProgrammable Custom Computing Machines (FCCM’03), pp. 31 – 38, April 2003.
[10] S. Dharmapurikar, P. Krishnamurthy, T. Sproull, J. Lockwood, “Deep packet inspection
using parallel bloom ﬁlters,” in Proc. of 11th IEEE Symp. on High Performance Interconnects (HotI ’03), pp. 44 – 51, August 2003.
[11] Z. K. Baker, V. K. Prasanna, “Time and Area Eﬃcient Pattern Matching on FPGAs,”in Proc. of the 2004 ACM/SIGDA 12th Intl. Symp. on Field programmable gate arrays(FPGA’04), pp. 223–232, February 2004.
[12] A. V. Aho, M. J. Corasick, “Eﬃcient String Matching : An Aid to Bibliographic Search,”
Communications of the ACM, vol. Vol. 18, pp. 333 – 340, June 1975.

11