Nowadays, it is di cult to describe any algebraic dynamic structures that usually includes the notion of state. A suitable structure for describing these systems can be a coalgebra, properties of which are dual to algebraic by their modeling in terms of category theory. This paper presents our approach for a formal description of a program system behavior based on category theory, coalgebr and coalgebraic logic. At the beginning, we brie y present basic notions from mentioned formal methods, and then we present motivation example from the area of the operating system GNU/Linux by its system calls.
Coalgebr are useful categorical structures with many applications in computer science. In our approach, they are used for modeling state oriented behavior of program systems.
Many logical systems, which are used in computer science, are derivations of modal logics. In our paper we present one of them, which is based on category theory and coalgebr , named coalgebraic logic. Its rst de nition came from Moss [Mos97]. It is necessary for de nition of this logical system to de ne category of classes and polynomial endofunctor over such a category.
Coalgebraic logic, with its expressive power, has a wide use in computer science through its formul , for example, specifying non-well founded abstract data structures [Kur01], in nite data structures [Kur00], or observation of program systems behavior [Mih14].
Our recent works regarding coalgebr [Mih12], [Mih14], [Per15] were oriented to modeling of intrusion detection system behavior as coalgebra for an appropriate endofunctor over category of in nite packet stream. We present in this work several fruitful aspects about coalgebraic logic and its role in a formal description of program behavior.
In: E. Vatai (ed.): Proceedings of the 11th Joint Conference on Mathematics and Computer Science, Eger, Hungary, 20th { 22nd of May, 2016, published at http://ceur-ws.org 2.1
Category theory Category theory was founded in 1945 by Eilenberg's and MacLane's work as a part of their research in the eld of algebraic topology [Mac45], where they formulated a notion of categories, functors and natural transformations of functors, as a formalism for describing mathematical structures. Nowadays [Mih10], category theory is a universal abstract mathematical frame used for description of various structures as mathematical, algebraic, or abstract data structures used in computer science.
According to [Bar98], [Jac97], a category C is a mathematical structure which consists of: a class of objects Co 2 C, where Co = fX; Y; Z : : : g and a class of morphisms between objects Cm 2 C, where Cm = ff; g; h : : : g.
Every category C possesses the following well de ned properties:
If there is a morphism f 2 Cm between two objects X; Y 2 Co from the object X to the object Y it is denoted as f : X ! Y .
Lets have a morphism f 2 Cm de ned as f : X ! Y . Then object X 2 Co is a domain of a morphism and object Y 2 Co is its codomain.
For every object X 2 Co there is an identity morphism idX 2 Cm de ned as: idX : X ! X, where domain and codomain of such a morphism is X.
The most important property of every category C is that morphisms are composable i.e. lets have X; Y; Z 2 Co and two morphisms f; g 2 Cm de ne as follows: f : X ! Y and g : Y ! Z, then there is a morphism g f : X ! Z.
Typical example of a category is the category of classes SET, where objects are represented as sets and morphisms as functions between them. 2.2
Functors Many mathematical structures can be modeled as categories [Ste14]. Since categories are also mathematical structures [Kur01], one should consider a category of categories, where objects are categories and morphisms of such a category are a structure preserving maps between categories, called functors.
Let C and D be categories and F : C ! D be a functor. Then F is a morphism from the source category C to the destination category D [Kur00]. A functor F assigns to every object X 2 C an object F (X) 2 D. Also a functor F assigns to every morphism f : X ! Y 2 C a morphism F (f ) : F (X) ! F (Y ) 2 D satisfying following conditions: for every object X 2 C and its identity object morphism idX : X ! X there is for every two morphisms f; g 2 C a functor F preserves composition properties (g f ) such as:
F (idX ) = idF (X);
F (g f ) = F (g) F (f ): This kind of functors is called simple [Bar98]. Another examples of simple functors are: identity functor IDC : C ! C; endofunctor E : C ! C, where source and destination category are the same.
In our approach, we use a special kind of endofunctor called polynomial endofunctor [Per15], [Mih12], [Slo11]. A polynomial endofunctor over category C is an endofunctor formed by polynomial operations shown in BackusNaur form (BNF) production rule as follows:
F (X) ::= XjX
Y jX + Y jXY :
(1) where
X is a coalgebra's state space of objects of category C and
is a morphism of category C such as : X ! F (X).
3
A plethora of current system behavior researches had shown the importance of choosing a suitable logical language. Those formul are used to logical reasoning over the states of the dynamic system. The states are captured by the coalgebra of an appropriate polynomial endofunctor.
Based on our previous work, in this chapter we present logical system based on multimodal language. It is suitable for description of the behavior of in nite data structures. This logic is called the coalgebraic logic introduced by Moss in his work [Mos97]. For its de nition, it is necessary to de ne the category of classes SET and polynomial endofunctor over it as F : SET ! SET:
Note 3.1: Since we won't be manipulating only with formul and sets of formul [Bil13], but also with elements of F!L!, it is bene cial to use the convention of notations from the table 1. To be more transparent, we will use notation F! for polynomial endofunctor instead of F . Coalgebr are useful categorical structures in computer science [Mac11], [Sma11]. In our approach we use them for modeling state oriented behavior of program systems.
Lets have a category C and polynomial endofunctor F [Kur01], [Mos97], [Kur00], then a coalgebra for a polynomial endofunctor F (sometimes also called F -coalgebra) is formally an ordered pair: Kurz in his work [Kur01] says that the main reason for introduction of the coalgebraic logic is to nd a modal language L! for every coalgebra (X; ) and to specify its satis ability relation as follows
Set
L! F!L!
'; ; : : :
; ; : : : ' ::= ? j > j :' j ^
j r ; where if if
L!,
L!, if ' 2 F!L!, then then then ^
2 L!; :' 2 L!; (3) (4)
From the production rule (4), it is clear that formul of coalgebraic logic are ordered pairs or their in nite conjunctions [Mih10]. While the modality r means shorthand notation where ^; _ are in nite forms of conjunction and disjunction. The following equivalences are valid: r }' ' _ ^ ^} ; rf'; >g r _ rf'g
Example 3.1.1 Let F!X = A Then the formul
X and ai 2 A, i 2 N. are formul
of coalgebraic logic. 3.2
Semantics of coalgebraic logic
(>); (a0; >); (a0(a1; >); : : : ; ^f(a0; a1; : : : ; an; >) j n 2 Ng Let (X; ) be a coalgebra and x 2 X. Then according to [Kur00] the semantics of coalgebraic logic can be expressed by the following satis ability relation as follows: where 1; 2 are projections of product X
L!. 4
We present traceability of intrusion system calls of a running functional program under the OS GNU/Linux as a demonstration example [Mra13]. We understand system calls as in nite stream, therefore it is suitable to model them as coalgebra for a polynomial endofunctor. We also specify system calls as formul of coalgebraic logic. 4.1
Many-typed coalgebraic signature of system calls First, we de ne many-typed coalgebraic signature of system calls. Formally it is an ordered pair where
T is a class of types names and F is a class of names of operations over types.
= (T ; F );
(5)
(6)
(7)
(8)
(9)
(
s Begin types
T = faction; char; hex; int; natg end Begin opns
F = falert; access; overflow :! actions, name :! char, arguments :! char, rt sigproc : char nat char nat ! int, rt sigprocmask :! int, clock gettime :! int, clone : char char char ! nat, timer set : int int char char mmap : char nat char char munmap : hex nat, wr rd : nat char nat ! int, open : char char nat ! int, setuid : int ! int, returnV alue :! int, nReturnV alue :! nat, hReturnV alue :! hex g char ! int; nat int ! hex,
The names of basic types from the class T in signature s de ne types of observed system calls [Mra13]. Operational speci cations, from the class F in signature s, de ne the structure (syntax) of individual system calls. The description of individual system calls is speci ed in the table 2. In the second step, we construct a category of system calls Scalls [Mra13], where objects are system calls s1; s2; : : : ; morphisms next : si ! si+1 are transition into the next system call of a given stream. 4.3
Polynomial endofunctor over category of system calls We specify a polynomial endofunctor over a category of system calls Scalls [Mra13] as follows We de ne actions of the endofunctor as follows
E : Scalls ! Scalls:
E(s) : O
s; : : : next- s2 next s5 next next Finally we model a stream of system calls as a coalgebra for a polynomial endofunctor. For demonstration we present two intrusion system call sequences.
A denotes Overloading of HW resources in this case by fork processes [Mra13]. Symptoms of this disruption are placed in a generated stream of system calls, where the system calls are repeated sequentially: name = rt sigprocmask ; nReturnValue = 0 name = clock gettime ; nReturnValue = 0 name = clock gettime ; nReturnValue = 0 name = clock gettime ; nReturnValue = 0 name = rt sigprocmask ; nReturnValue = 0 . . . . name = open, nReturnValue = -1 access to le name = write; wr rd = nat, char, 4 ; nReturnValue = 63 unauthorized writing to le name = read; wr rd = nat, char, 2 ; nReturnValue = 68 unauthorized reading to le B denotes Permission denied i.e. security violation of the stored data. Symptoms of this disruption are placed in the following generated stream of system calls.
Coalgebra (system) observes a stream of system calls and if it detects symptoms of disruption, then it responds by making one of the following preferred (re)actions (actions from the s) [Mra13], such as: Alert - generates attention on the screen; Wrong - unauthorized access, which saves output into appropriate log le and
Over ow - indication of the resource misuse, i.e. termination of whole implementation (EXIT FAILURE).
In the last step [Mra13], we de ne coalgebra with the detection of intrusion system activities as follows
(ss; hhd; tl; N signali);
(
Speci cation of the stream of system calls by coalgebraic logic The formul of coalgebraic logic are used for logical reasoning over states of a dynamic system that is captured by the coalgebra for a polynomial endofunctor [Mih14]. Now we specify in nite stream of system calls as formul of the modal language de ned in the section 3.
The application of coalgebraic speci cation creates an in nite sequence of coalgebraic formul (>) (s1; >) (s1; (s2; >)) (s1; (s2; (s3; >)))
: : : ^f(s1; (s2; (s3; (: : : ; (: : : ; >) : : : ))))g where the rst line (>) denotes an empty sequence, which is the initial state of the system. The second line rises after the rst application of coalgebraic speci cation. It speci es the initial (starting) system call. The next lines describe iterative application of coalgebraic speci cation up to a possible in nite sequence. 4.6
Example of detected intrusion system call Behavior of the system can be modeled step by step by the following sequence 7! 7! 7! (sstart; s : : : ) 7! ((srt sigproc; sclock gettime; sclock gettime; sclock gettime; srt sigproc); ) 7!10 ((srt sigproc; sclock gettime; sclock gettime; sclock gettime; srt sigproc); A 7! Alert ) 7! . . .
In this example, stream starts with the system call s start : : : , which represents initialization system calls of
a real system tool for system calls tracing (Strace) [Mra13]. Next system calls s timer set, s clone are speci c
types of system calls. The coalgebra observes the stream and detects intrusion of the type A and responds by
the action Alert ). The appropriate sequence of a real system calls is:
(
Initialization of Strace system calls. ... rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0 clock_gettime(CLOCK_THREAD_CPUTIME_ID, {0, 4854270}) = 0 clock_gettime(CLOCK_MONOTONIC, {2935465, 569821866}) = 0 clock_gettime(CLOCK_PROCESS_CPUTIME_ID, {0, 4817026}) = 0 rt_sigprocmask(SIG_BLOCK, [INT], [], 8) = 0 ...
Similarly, we can model the B or any known intrusion system call. 5
In this contribution we brie y present basic notions from category theory, coalgebr and coalgebraic logic. We demonstrate our approach of a formal description of program systems behavior on the example from operating system's GNU/Linux detection and handling of intrusion system calls.
We see a possibility in creating veri able model, using mathematical formal methods to develop intrusion detection systems by observing their behavior. Based on this, it is possible to eliminate undesirable behavior and, with a combination of host and network intrusion detection systems, to create a complex security for program systems.
In the future, we would like to extend our approach by joining the network intrusion detection systems with a host-based one. A combination of both types of IDSs will allow us to secure computer systems even more. Next step in our work will be extending IDS by applying the resource oriented Belief-Desire-Intention logical system, that will allow automated IDSs reactions, instead of a system administrator intervention. Another idea for our future work is an application of a self-healing code procedures, which would allow a detection and handling of even new and unknown intrusions.
Acknowledgment This paper was supported by KEGA project ViLMA: Virtual Laboratory for Malware Analysis (079TUKE04/2017).
This work is a result of international cooperation under the CEEPUS network No.CIII-HU-0019-12-1617. [Bar98]
M. Barr, and C. Wells. Category theory for computing science. Prentice Hall International (UK) Ltd., 66 Wood Lane End, Hertfordshire, UK, 1998.
M. Bilkova, A. Palmigiano, and Y. Vemena. Proof systems for Moss coalgebraic logic. Theoretical Computer Science (2013), pp. 36-60. - ISSN 0304-3975 [Kur01] A. Kurz. Coalgebr
and Modal Logic. CWI, Amsterdam, Netherlands, 2001 [Kur00] A. Kurz. Logics for coalgebr
Netherlands, 2000
and applications to computer science. Dissertation thesis, Amsterdam,
B. Jacobs, and J. Rutten. A tutorial on (co) algebras and (co) induction. Bulletin-European Association for Theoretical Computer Science, vol. 62, pp. 222-259, 1997. [Mac45] S. Eilenberg, and S. Mac Lane. General theory of natural equivalences. Trans. Am. Math. Soc., vol. 58, pp. 231294, 1945. [Slo11]
V. Slodicak, and P. Macko. Some new approaches in functional programming using algebras and coalgebr . Electronic Notes in Theoretical Computer Science, vol. 279, no. 3, pp. 4162, 2011. [Mac11] V. Slodicak, and P. Macko. The rle of linear logic in coalgebraical approach of computing. Journal of Information and Organizational Sciences, vol. 35, no. 2, pp. 197213, 2011. [Ste14]