Hacking the Linux Kernel in Ada

Hacking the Linux Kernel in Ada(linux.com)

9 points by KlatchianMist 4 years ago | 3 comments

theamk 4 years ago |

It is interesting how few modern features Ada has... Author talks about strict types, and this is an improvement, but other than that, it is still unsafe C:

    if Wq = K.Null_Wq then -- Ada equal
       Wq := K.Create_Singlethread_Wq ("flash_led_wq");
    end if;
    
    if Wq /= K.Null_Wq then -- Ada not equal
       K.Queue_Delayed_Work(Wq,

What if programmer forgets this "Wq = K.Null_Wq" check? Then we get a memory leak. What if they omit the next check? Then we get null pointer dereference if allocation fails.

For all that fancy types Ada has, it is still plain pointers underneath. There are no destructors to release resources, no fancy error handling to avoid types.

Extra "unsafety" points in these series: "printk" security vulnerabilities, and standard headers re-implementation that'll likely break in subtle ways in future kernel versions.

olivier_henley 4 years ago | |

Author here.

- What if ... forgets this "Wq = K.Null_Wq" check : The goal was to KISS. Air bagging such trivial code never crossed my mind in regard to the original intent; Share Ada's raw power, no fuss.

- ... still plain pointers underneath ...: Well when you need to survive, the dirty blade is still an option. That is what keeps it so powerful too. If there were no pointers, another pal would come and say: "aargh, another sandboxed language...". Actually, Ada is healthy about pointers and I would think twice before getting rid of them completely.

- There are no destructors ...: Well yes, controlled types. You are welcome to give a try to bring them in kernel space. I did not have the time to even try. Maybe it is low hanging, really I dont know.

- Extra "unsafety"... "printk" security vulnerabilities : Were there claims to harden the Linux API? I do not recall.

- Extra "unsafety"... re-implementation ... likely break : To be fair, I think I repeated three times in the series a version of "we do not recommend re-implementation, reconstruction of APIs. wrappers inherit fixes, its only to show nuts and bolts, etc"

With all due respect, I think you should at least re-read the introduction and the "Linux Driver Experiment In Ada, But Why?" section. It gives a good common sense view of the intended scope of the series: no more, no less.

With all that said, addressing your points would make an interesting follow-up series. Maybe if I find the time or you decide to take up on the task we could see where it leads!

Thanks for chipping in.

yannickmoy 4 years ago | |

You can get automatic resource handling with controlled types, but this is not part of the baremetal minimal runtime you can use for a driver.

You can get ownership tracking with SPARK, but you need to use proof techniques.

There are pointers in Ada, but it's not at all the same as in C. First, C pointers are really addresses, references and pointers in Ada. And pointers come in various flavors named/anonymous access-to-variable/constant/subprogram, pointing only to the heap or also to the stack, with accessibility levels depending on where the type is defined... which lead to fine-grain distinction of the various use cases with SPARK so that only correct use is provable.