1. CrytoLocker

  • A ransomware trojan
    • Targeted computers running Microsoft Windows.
    • First observed by Dell SecureWorks in September 2013 (CryptoLocker).
  • Principle
    • It breaks into the system,
    • Infects specific files, and
    • Demands ransom for recovery from the infection.


2. Configuration: Processes in CryptoLocker

  • System consists of two parts:

    • S and its internal components:

      • S contains E, to search files in the system.

      • Other various processes.

    • The other to give permission for an external process to enter S.

      • Other processes except E have the same priority of m. 

3. δ-Calculus


  • System∷=S_((0) ) [E_((0) )∥P1_((m) )∥P2_((m) )∥ P3_((m) )∥…∥Pn_((m) ) ]〈SYS,NET〉∥(F in)^∞
  • F∷=P1∥P2∥P3∥…∥CL∥CP∥…
  • CL∷=in_t1  S.new I.new D.nil
  • D∷=kill CL.exit     
  • I∷=(in) ̅_t2^p  E.W
  • W∷=nil△_∞ (nil,nil,SYS(trigger).NET((download) ̅ ).W)
  • CP∷=NET(download).in_t3  S.new K.(get) ̅_t4^p  K.(get_tj^p  Pi.new Pi^′.kill Pi)^n.(SYS.((ReqM) ̅ ).SYS(sendM))△_t5 (OP,kill K.exit,nil)
  • OP∷=(get_tk^p  Pi^′.new Pi.kill Pi^′ )^n.exit


4. Operational  Requirements


1) After CL enters S, CL creates I and D processes.
2) D terminates CL and terminates itself.
3) I enters E forcibly by priority-based asynchronous movement, becomes a Hide process of E, and waits in the W state.
4) f Trigger is met by a specific action of S, W downloads CP by a port of S, NET.
5) When CP is downloaded and entered in S, it creates a key outside of S and brings the key in.
6) CP brings other processes in it, creates the enciphered version of the processes with the key, and forcibly terminates the original version of the processes.
7) Once the enciphering is done, demand ransom through the system S with a deadline.
8) If the ransom is paid in time, the enciphering is terminated and all the enciphered processes are recovered.
9) If the ransom is not paid in time, CP deletes the key and terminates itself.

3. ITL View


CL_ITL_TOOL.png


4. ITS View


CL_ITS_TOOL1.png


CL_ITS.png



5. Execution Model


CL_EM.png



6. Simulation/GTS


1) Normal Case


Abnormal-norel-tool.png


Abnormal-noreq.png


2) Abnormal Case: Deadlock


Deadlock1-norel-tool.png


Deadlock1-noreq.png


7. GTS Logic


1) Requirements


  • The (new I) and (new D) actions of CL should be executed after the (in S) movement action of CL.
    • δ_(CL,S)<CL:(new I)∧CL:(new D)
    • CL:(in S)<CL:(new I)∧CL:(new D)
  • The (kill CL) action of D should be executed after the movement of I, that is, the (put I) movement action of CL.
    • δ_(CL,I)<D:(kill CL)
    • CL:(put I)<D:(kill CL)
  •  K should be in CP all the time.
    • K⊂CP


2) Normal Case


Abnormal-full-tool.png


Abnormal-full.png


3) Abnormal Case


Deadlock1-full-tool.png


Deadlock1-full.png


이 게시물을